diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v
index 0f23113..2c02807 100644
--- a/ConcurrentSeparationLogic.v
+++ b/ConcurrentSeparationLogic.v
@@ -698,7 +698,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.
@@ -823,7 +823,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.
diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v
index 96acab4..3f9d7cb 100644
--- a/ConcurrentSeparationLogic_template.v
+++ b/ConcurrentSeparationLogic_template.v
@@ -743,7 +743,7 @@ Proof.
   simp.
   rewrite Heq in H0.
   simp.
-  equality.
+  try equality.
   cancel.
   cancel.
   cancel.