proposition: Lemma map2_or_comm: forall (a b: list bool), (map2 orb a b) = (map2 orb 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 orb_comm. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance