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