# ReverseReverse2 by Lost_dog_

module Theorem where
open import Definitions
open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
lem : ∀ {a} {A : Set a} (a : A)(as : List A) → myreverse (as ∷ʳ a) ≡ a ∷ myreverse as
lem a [] = refl
lem a (x ∷ xs)
rewrite unfold-reverse x xs
| unfold-reverse x (xs ∷ʳ a)
| lem a xs
= refl
revrev : ∀ {a} {A : Set a} (as : List A) → myreverse (myreverse as) ≡ as
revrev [] = refl
revrev (x ∷ xs)
rewrite unfold-reverse x xs
| lem x (reverse xs)
| revrev xs
= refl