proposition: Lemma map2_xor_length: forall (a b: list bool), length a = length b -> length a = length (map2 xorb a b).
proof: Proof. induction a as [ | a' xs IHxs]. simpl. auto. intros [ | b ys]. - simpl. intros. exact H. - intros. simpl in *. apply f_equal. apply IHxs. inversion H; auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance