reverse (reverse xs) ≡ xs in Agda

gistfile1.txt

{-# OPTIONS --universe-polymorphism #-}
module ReverseReverseId where

open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality 
  as P using (_≡_; refl; cong)

ReverseReverseId : ∀ {a} {A : Set a} (xs : List A) -> 
                   reverse (reverse xs) ≡ xs
ReverseReverseId [] = refl
ReverseReverseId (x ∷ xs) = 
  begin
    reverse (reverse (x ∷ xs)) 
      ≡⟨ cong (λ zs → reverse zs) (unfold-reverse x xs) ⟩ 
    reverse (reverse xs ++ [ x ]) 
      ≡⟨ reverse-++-commute (reverse xs) [ x ] ⟩ 
    reverse [ x ] ++ reverse (reverse xs) 
      ≡⟨ cong (λ zs → reverse [ x ] ++ zs) (ReverseReverseId xs) ⟩ 
    reverse [ x ] ++ xs ≡⟨ refl ⟩ 
    x ∷ xs
  ∎
  where open P.≡-Reasoning