proposition: Lemma map2_xor_assoc: forall (a b c: list bool), (map2 xorb a (map2 xorb b c)) = (map2 xorb (map2 xorb a b) c).
proof: Proof. intro a. induction a as [ | a' xs IHxs]. simpl. auto. intros [ | b' ys]. - simpl. auto. - intros [ | c' zs]. + simpl. auto. + simpl. cut (xorb a' (xorb b' c') = (xorb (xorb a' b') c')). intro H. rewrite <- H. apply f_equal. apply IHxs. rewrite xorb_assoc_reverse. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance