# ReverseReverse3 FIXED by trigott

module Theorem where
open import Definitions
open import Data.List
open import Relation.Binary.PropositionalEquality
lem₁ : ∀ {a} {A : Set a} (tl : A) (xs rest : List A) →
rev xs (rest ∷ʳ tl) ≡ rev xs rest ∷ʳ tl
lem₁ tl [] rest = refl
lem₁ tl (x ∷ xs) rest = lem₁ tl xs (x ∷ rest)
lem₂ : ∀ {a} {A : Set a} (x : A) (xs rest : List A) →
rev (xs ∷ʳ x) rest ≡ x ∷ rev xs rest
lem₂ x [] rest = refl
lem₂ x (y ∷ xs) rest = lem₂ x xs (y ∷ rest)
revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (x ∷ xs)
rewrite (lem₁ x xs [])
| (lem₂ x (rev xs []) []) = cong (_∷_ x) (revrev xs)