# ReverseReverse2 by trigott

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