diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam
index efd8584..cb66c82 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: "20240904"
+version: "20240916"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
   "dune" {>= "3.7"}
diff --git a/theories/Common/Capabilities.v b/theories/Common/Capabilities.v
index e8db3a2..5de7229 100644
--- a/theories/Common/Capabilities.v
+++ b/theories/Common/Capabilities.v
@@ -332,8 +332,7 @@ Module Type CAPABILITY
   Parameter cap_encode_length:
     forall c l t, encode c = Some (l, t) -> List.length l = sizeof_cap.
 
-  Parameter cap_exact_encode_decode:
-    forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true.
-
+  Parameter cap_encode_decode:
+    forall cap bytes t, encode cap = Some (bytes, t) -> decode bytes t = Some cap.
 
 End CAPABILITY.
diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v
index e83d6a8..84e69e7 100644
--- a/theories/Morello/Capabilities.v
+++ b/theories/Morello/Capabilities.v
@@ -1403,7 +1403,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
       reflexivity.
   Qed.
 
-  (* Consider migrating these functions to the libraries where the functions that reason about are defined *)
+  (* Consider migrating these functions to the libraries where the functions they reason about are defined *)
   Lemma byte_chunks_len {a} (l : list a) l'  :
     (8 | length l)%nat → 
     byte_chunks l = Some l' → 
@@ -1538,7 +1538,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     @mword_to_bools 129 c = (((@bv_extract 129 128 1 c =? 1)) :: (@mword_to_bools 128(@bv_extract 129 0 128 c)))%list.
   Admitted.
 
-  Lemma cap_exact_encode_decode :
+  Lemma cap_exact_encode_decode_weak :
     forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true.
   Proof.
     intros c c' t l E D. apply eqb_eq.
@@ -1572,6 +1572,13 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
       unfold MachineWord.word_to_N; rewrite Z2N.id; [ done | apply bv_unsigned_in_range ].
   Qed.
 
+  Lemma cap_encode_decode:
+    ∀ cap bytes t,
+      encode cap = Some (bytes, t) → 
+      decode bytes t = Some cap.
+  Proof. 
+  Admitted.
+
 End Capability.