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