diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 6f72f4fe2756b5d56e28b8a7dba6a5f1fd39569d..a4665d1ff42481da888bf527c7454395144d31b9 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -145,9 +145,8 @@ Section cell.
     typed_val cell_new (fn(∅; ty) → cell ty) (λ post '-[a], Φ a ∧ post Φ).
   Proof.
     eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
-    { iApply type_jump; [solve_typing| |].
-      { eapply tctx_extract_ctx_elt; [apply tctx_cell_new|solve_typing]. }
-      solve_typing. }
+    { iApply type_jump; [solve_typing| |solve_typing].
+      eapply tctx_extract_ctx_elt; [apply tctx_cell_new|solve_typing]. }
     by move=> ?[?[]]?/=.
   Qed.
 
@@ -175,9 +174,8 @@ Section cell.
       (λ post '-[Φ], ∀a: 𝔄, Φ a → post a).
   Proof.
     eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
-    { iApply type_jump; [solve_typing| |].
-      { eapply tctx_extract_ctx_elt; [apply tctx_cell_into_inner|solve_typing]. }
-      solve_typing. }
+    { iApply type_jump; [solve_typing| |solve_typing].
+      eapply tctx_extract_ctx_elt; [apply tctx_cell_into_inner|solve_typing]. }
     by move=> ?[?[]]?/=.
   Qed.
 
@@ -206,9 +204,8 @@ Section cell.
       (λ post '-[a], Φ a ∧ post Φ).
   Proof.
     eapply type_fn; [apply _|]=> _ ??[?[]]. simpl_subst. via_tr_impl.
-    { iApply type_jump; [solve_typing| |].
-      { eapply tctx_extract_ctx_elt; [apply tctx_cell_from_box|solve_typing]. }
-      solve_typing. }
+    { iApply type_jump; [solve_typing| |solve_typing].
+      eapply tctx_extract_ctx_elt; [apply tctx_cell_from_box|solve_typing]. }
     by move=> ?[?[]]?/=.
   Qed.