proposition: Lemma not_list_and_or: forall a b, map negb (map2 andb a b) = map2 orb (map negb a) (map negb b).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - auto. - intros [ | b ys]. + auto. + simpl. rewrite negb_andb. apply f_equal. apply IHxs. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance