proposition: Lemma bv_xor_assoc : forall n (a b c :bitvector n), bv_eq (bv_xor a (bv_xor b c)) (bv_xor (bv_xor a b) c) = true.
proof: Proof. intros n a b c. unfold bv_eq. rewrite M.bv_eq_reflect. simpl. apply (@M.bv_xor_assoc n a b c); now rewrite wf. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance