proposition: Lemma rev_eq: forall x y, beq_list x y = true -> beq_list (List.rev x) (List.rev y) = true.
proof: Proof. intros. apply List_eq in H. rewrite H. now apply List_eq_refl. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance