proposition: Lemma map2_xor_empty_empty1: forall (a: list bool), (map2 xorb a []) = [].
proof: Proof. intros a. induction a as [ | a' xs IHxs]; simpl; auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance