proposition: Lemma map2_and_comm: forall (a b: list bool), (map2 andb a b) = (map2 andb b a).
proof: Proof. intros a. induction a as [ | a' xs IHxs]. intros [ | b' ys]. - simpl. auto. - simpl. auto. - intros [ | b' ys]. + simpl. auto. + intros. simpl. cut (a' && b' = b' && a'). intro H. rewrite <- H. apply f_equal. apply IHxs. apply andb_comm. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance