ReverseReverse3 FIXED by Rotsor

module Theorem where
open import Definitions
open import Data.List
open import Relation.Binary.PropositionalEquality
revrev : ∀{a}{A : Set a}{a : List A}(x : List A)→ rev(rev x a)[] ≡ rev a x
revrev [] = refl
revrev (_ ∷ xs) = revrev xs