reverse (reverse xs) ≡ xs in Coq

gistfile1.txt

Require Import Coq.Lists.List.

Lemma rev_Unfold : forall {A:Type} (l:list A) (a:A), rev (a::l) = rev l ++ (cons a nil).
Proof.
intros.
simpl.
reflexivity.
Qed.

Theorem rev_Involutive : forall {A:Type} (l:list A), rev (rev l) = l.
Proof.
intros.
induction l.
reflexivity.
rename IHl into InductiveHypothesisOfl.
rewrite rev_Unfold.
rewrite rev_app_distr.
simpl.
rewrite InductiveHypothesisOfl.
reflexivity.
Qed.