proposition: Lemma map2_and_idem2: forall (a b: list bool), (map2 andb (map2 andb a b) b) = (map2 andb a b).
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' && b'). intro H. rewrite H. apply f_equal. apply IHxs. rewrite <- andb_assoc. rewrite andb_diag. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance