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