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)