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