proposition: Lemma map2_and_idem_comm: forall (a b: list bool), (map2 andb (map2 andb a b) a) = (map2 andb b a).
proof: Proof. intros a b. symmetry. rewrite <- map2_and_comm. symmetry; apply map2_and_idem1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance