proposition: Lemma map2_or_1_true: forall (a: list bool), (map2 orb a (mk_list_true (length a))) = (mk_list_true (length a)).
proof: Proof. intro a. induction a as [ | a' xs IHxs]. - simpl. reflexivity. - simpl. rewrite IHxs. rewrite orb_true_r; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance