proposition: Lemma rev_neq: forall x y, beq_list x y = false -> beq_list (List.rev x) (List.rev y) = false.
proof: Proof. intros. specialize (@List_neq x y H). intros. apply not_true_is_false. unfold not in *. intros. apply H0. apply List_eq in H1. specialize (f_equal (@List.rev bool) H1 ). intros. now rewrite !rev_involutive in H2. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance