proposition: Lemma map2_and_1_neutral: forall (a: list bool), (map2 andb a (mk_list_true (length a))) = a.
proof: Proof. intro a. induction a as [ | a xs IHxs]. + auto. + simpl. rewrite IHxs. rewrite andb_true_r. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance