proposition: Lemma List_neqP : forall (l m: list bool), ~beq_listP l m -> l <> m.
proof: Proof. intro l. induction l. - intros. case m in *; simpl. now contradict H. easy. - intros. unfold not in H. simpl in H. case_eq m; intros. easy. rewrite H0 in H. unfold not. intros. apply H. inversion H1. split; try easy. now apply List_eqP_refl. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance