diff --git a/theories/simulang/logical_heap.v b/theories/simulang/logical_heap.v
index 44bd5ba29ac0044eeec8c78ce1e6c704ff5808fc..4f5a9f8d4e1d8b6462bceb91ba7d02102df2282b 100644
--- a/theories/simulang/logical_heap.v
+++ b/theories/simulang/logical_heap.v
@@ -113,7 +113,7 @@ Section to_heap.
   Implicit Types σ : gmap loc (lock_state * val).
 
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+  Proof. intros l. rewrite lookup_fmap. case: (σ !! l)=> [[[|n] v]|] //=. Qed.
 
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
diff --git a/theories/stacked_borrows/type.v b/theories/stacked_borrows/type.v
index 23bec750665ead64bfe751320488ba6eb73512aa..af14372236dad7f9c27e422677fa47c4dcef7688 100644
--- a/theories/stacked_borrows/type.v
+++ b/theories/stacked_borrows/type.v
@@ -263,10 +263,10 @@ Proof.
      | GenNode 5 Ts => Sum (go <$> Ts)
      | _ => FixedSize 0
      end) _).
-  fix FIX 1. intros [| | |Ts|Ts|Ts]; f_equal=>//; revert Ts; clear -FIX.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
+  fix FIX 1. intros [| | |Ts|Ts|Ts]; csimpl; f_equal=>//; revert Ts; clear -FIX.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
 Qed.
 
 (** Finding sum types *)