diff --git a/heapster-saw/examples/xor_swap_proofs.v b/heapster-saw/examples/xor_swap_proofs.v
index 2114d9ed90..e6c3ca5ac6 100644
--- a/heapster-saw/examples/xor_swap_proofs.v
+++ b/heapster-saw/examples/xor_swap_proofs.v
@@ -4,6 +4,7 @@ From Coq          Require Import String.
 From Coq          Require Import Vectors.Vector.
 From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
 
 From CryptolToCoq Require Import SAWCorePrelude.
 From CryptolToCoq Require Import CompMExtra.
@@ -23,19 +24,19 @@ Proof.
   time "no_errors_xor_swap" prove_refinement.
 Qed.
 
-(* FIXME: move lemma to SAWCorePrelude...? *)
+
 Lemma bvXor_twice_r n x y :
   SAWCorePrelude.bvXor n (SAWCorePrelude.bvXor n x y) y = x.
 Proof.
-  admit.
-Admitted.
+  rewrite <- bvXor_assoc. rewrite bvXor_same. rewrite bvXor_zero. reflexivity.
+Qed.
 
-(* FIXME: move lemma to SAWCorePrelude...? *)
 Lemma bvXor_twice_l n x y :
   SAWCorePrelude.bvXor n (SAWCorePrelude.bvXor n y x) y = x.
 Proof.
-  admit.
-Admitted.
+  rewrite bvXor_comm. rewrite bvXor_assoc.
+  rewrite bvXor_same. rewrite bvXor_comm. rewrite bvXor_zero. reflexivity.
+Qed.
 
 Lemma xor_swap_correct : refinesFun xor_swap xor_swap_spec.
 Proof.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index af2d4cb0be..cfda7581f4 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -16,7 +16,7 @@ Import SAWCorePrelude.
 
 (* A duplicate from `Program.Equality`, because importing that
    module directly gives us a conflict with the `~=` notation... *)
-Tactic Notation "dependent" "destruction" ident(H) := 
+Tactic Notation "dependent" "destruction" ident(H) :=
   Equality.do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => Equality.do_case hyp) H.
 
 Create HintDb SAWCoreBitvectors_eqs.
@@ -229,6 +229,51 @@ Admitted.
 Lemma bvule_msb_r w a b : isBvule (Succ w) a b -> msb w b = false -> msb w a = false.
 Admitted.
 
+(** Lemmas about bitvector xor **)
+
+Lemma bvXor_same n x :
+  SAWCorePrelude.bvXor n x x = SAWCorePrelude.replicate n Bool false.
+Proof.
+  unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith, SAWCorePrelude.replicate.
+  induction x; auto; simpl; f_equal; auto.
+  rewrite SAWCorePrelude.xor_same; auto.
+Qed.
+
+Lemma bvXor_zero n x :
+  SAWCorePrelude.bvXor n x (SAWCorePrelude.replicate n Bool false) = x.
+Proof.
+  unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith, SAWCorePrelude.replicate.
+  induction x; auto; simpl. f_equal; auto; cbn.
+  rewrite SAWCorePrelude.xor_False2; auto.
+Qed.
+
+Lemma bvXor_assoc n x y z :
+  SAWCorePrelude.bvXor n x (SAWCorePrelude.bvXor n y z) =
+  SAWCorePrelude.bvXor n (SAWCorePrelude.bvXor n x y) z.
+Proof.
+  unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith.
+  induction n; auto; simpl. f_equal; auto; cbn.
+  unfold xor. rewrite Bool.xorb_assoc_reverse. reflexivity.
+  remember (S n).
+  destruct x; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
+  destruct y; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
+  destruct z; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
+  intros. subst. clear Heqn0. cbn. apply IHn.
+Qed.
+
+Lemma bvXor_comm n x y :
+  SAWCorePrelude.bvXor n x y = SAWCorePrelude.bvXor n y x.
+Proof.
+  unfold SAWCorePrelude.bvXor, SAWCorePrelude.bvZipWith, SAWCorePrelude.zipWith.
+  induction n; auto; simpl. f_equal; auto; cbn.
+  unfold xor. apply Bool.xorb_comm.
+  remember (S n).
+  destruct x; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
+  destruct y; try solve [inversion Heqn0; clear Heqn0; subst]. injection Heqn0.
+  intros. subst. clear Heqn0. cbn. apply IHn.
+Qed.
+
+
 
 (** Some general lemmas about boolean equality **)