# ReverseReverse3 FIXED by Lost_dog_

module Theorem where
open import Definitions
open import Algebra
open import Data.List
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
module LM {a} {A : Set a} = Monoid (monoid A)
myunfold-reverse : ∀ {a} {A : Set a} (x : A) (xs : List A) → myreverse (x ∷ xs) ≡ myreverse xs ∷ʳ x
myunfold-reverse x xs = begin
myreverse (x ∷ xs) ≡⟨ lem xs ([ x ]) ⟩
rev xs [] ∷ʳ x
∎
where
lem : ∀ {a} {A : Set a} (xs ys : List A) → rev xs ys ≡ myreverse xs ++ ys
lem [] ys = refl
lem (x ∷ xs) ys
rewrite lem xs (x ∷ ys)
| myunfold-reverse x xs
| LM.assoc (rev xs []) ([ x ]) ys
= refl
lem : ∀ {a} {A : Set a} (x : A) (xs : List A) → myreverse (xs ∷ʳ x) ≡ x ∷ myreverse xs
lem x [] = refl
lem x (x' ∷ xs)
rewrite myunfold-reverse x' (xs ∷ʳ x)
| myunfold-reverse x' xs
| lem x xs
= refl
revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (x ∷ xs)
rewrite myunfold-reverse x xs
| lem x xs
| lem x (myreverse xs)
| revrev xs
= refl