proposition: Lemma bv_xor_assoc: forall n a b c, (size a) = n -> (size b) = n -> (size c) = n -> (bv_xor a (bv_xor b c)) = (bv_xor (bv_xor a b) c).
proof: Proof. intros n a b c H0 H1 H2. unfold bv_xor. rewrite H1, H2. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. unfold size, bits in *. rewrite <- (@map2_xor_length b c). rewrite H0, H1. rewrite N.compare_refl. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite <- (@map2_xor_length a b). rewrite H0. rewrite N.compare_refl. rewrite map2_xor_assoc; reflexivity. now rewrite <- Nat2N.inj_iff, H0. now rewrite <- Nat2N.inj_iff, H1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance