ReverseReverse1 by Lost_dog_

module Theorem where

open import Definitions

open import Data.List
open import Relation.Binary.PropositionalEquality


lem : ∀ {a} {A : Set a} (x : A) (xs : List A) → myreverse (xs ∷ʳ x) ≡ x ∷ myreverse xs
lem x [] = refl
lem x (x' ∷ xs) rewrite lem x xs = refl

revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (x ∷ xs)
  rewrite lem x (myreverse xs)
        | revrev xs 
  = refl