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