proposition: Lemma map2_xor_empty_empty2: forall (a: list bool), (map2 xorb [] a) = [].
proof: Proof. intros a. rewrite map2_xor_comm. apply map2_xor_empty_empty1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance