diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam
index 64933ec..524394a 100644
--- a/coq-cheri-capabilities.opam
+++ b/coq-cheri-capabilities.opam
@@ -6,7 +6,7 @@ maintainer: ["ricardo.almeida@ed.ac.uk"]
 authors: ["Ricardo Almeida" "Vadim Zaliva"]
 license: "BSD-3-clause"
 homepage: "https://github.com/rems-project/coq-cheri-capabilities"
-version: "20240408"
+version: "20240521"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
   "dune" {>= "3.7"}
diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v
index e4783f6..31319a6 100644
--- a/theories/Morello/Capabilities.v
+++ b/theories/Morello/Capabilities.v
@@ -1027,6 +1027,33 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     - intro H. rewrite H. apply eqb_refl.
   Defined.  
   
+  Ltac unfold_cap :=
+    repeat 
+      (unfold Capability.cap_permits_load, Capability.cap_permits_store, Capability.cap_get_perms, Capability.cap_is_unsealed, Capability.cap_is_sealed, Capability.cap_get_value, Capability.cap_set_value; simpl;
+      unfold Capabilities.Permissions.has_load_perm, Capabilities.Permissions.has_store_perm, len, Capabilities.Permissions.has_perm; 
+      unfold AddressValue.t, AddressValue.len in *;
+      unfold CapFns.CapGetValue, CapFns.CapSetValue, CapFns.CapPermsInclude, CapFns.CapGetPermissions, CapFns.CAP_PERM_LOAD, CapFns.CAP_PERM_STORE, CapFns.CAP_PERMS_NUM_BITS, CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT, CapFns.integer_subrange, CapFns.CapIsSealed, CapFns.Zeros, CapFns.CapGetObjectType, CapFns.CAP_VALUE_NUM_BITS, CapFns.CAP_VALUE_HI_BIT, CapFns.CAP_VALUE_LO_BIT, CapFns.CAP_OTYPE_LO_BIT in *; simpl;
+      unfold Operators_mwords.get_slice_int, Operators_mwords.subrange_vec_dec, Operators_mwords.neq_vec, Operators_mwords.eq_vec, Operators_mwords.update_subrange_vec_dec; simpl;
+      unfold MachineWord.update_slice, MachineWord.MachineWord.slice, MachineWord.MachineWord.Z_to_word, MachineWord.MachineWord.and, MachineWord.MachineWord.eqb, MachineWord.MachineWord.eq_dec, MachineWord.MachineWord.zero_extend, MachineWord.MachineWord.zeros; simpl;
+      unfold Values.shl_int, Values.to_word_nat, Values.to_word, Values.get_word; simpl;
+      unfold TypeCasts.autocast; simpl; 
+      bv_simplify; 
+      change (63 - 0 + 1) with 64;
+      change (63 + 1)%positive with 64%positive;
+      change (Z.to_nat 0) with 0%nat;
+      change (Z.to_nat 64) with 64%nat;
+      change (Z.to_nat 110) with 110%nat;
+      change (Pos.to_nat 64) with 64%nat;
+      change (N.of_nat 0) with 0%N;
+      change (N.of_nat 18) with 18%N;
+      change (N.of_nat 64) with 64%N;
+      change (N.of_nat 110) with 110%N;
+      change (Z.to_nat 95) with 95%nat;
+      change (N.of_nat 15) with 15%N;
+      change (N.of_nat 95) with 95%N;
+      simpl;
+      bv_simplify).
+
   Lemma cap_invalidate_invalidates (c:t) : cap_is_valid (cap_invalidate c) = false.
   Proof.
     unfold cap_invalidate, cap_is_valid.
@@ -1098,6 +1125,17 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     bv_simplify. rewrite bv_extract_unsigned. rewrite bv_extract_unsigned. bv_simplify.  bitblast.       
     Qed.  
 
+  Lemma cap_get_set_value (c:t) (a:AddressValue.t) :
+    cap_get_value (cap_set_value c a) = a.
+  Proof.
+    unfold cap_get_value. unfold cap_set_value.
+    destruct (cap_is_sealed c); [ fold (cap_get_value (cap_invalidate (CapSetValue c a))); rewrite <- cap_invalidate_preserves_value; unfold cap_get_value | ];
+    unfold CapGetValue, CapSetValue; destruct (CapBoundsUsesValue _); simpl; try destruct (neq_vec _ _);
+      try rewrite <- subrange_vec_dec_after_clear_tag; try (unfold_cap; done);
+        unfold_cap; change (N.of_nat (Z.to_nat (63 - (0 - 1)))) with 64%N; bv_simplify; simpl; change (bv_unsigned a ≪ 0)%Z with (bv_unsigned a);
+        bitblast.
+  Qed. 
+    
   (* Lemma cap_invalidate_preserves_bounds (c:t) : cap_get_bounds c = cap_get_bounds (cap_invalidate c).
   Proof.
       Admitted. *)