diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index daf5f1d84ef139a1f672562209972229569224e1..48290a3fc8d1288b2ab80b9227b6e70ee30fc1ee 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -22,7 +22,7 @@ Section get_x.
 
     eapply type_let'.
     { apply _. }
-    { by apply (type_deref (&uniq{α}Π [int; int])), read_own_move. }
+    { by eapply (type_deref (&uniq{α} _)), read_own_move. }
     { solve_typing. }
     intros p'. simpl_subst.
 
@@ -30,7 +30,7 @@ Section get_x.
 
     eapply type_let'.
     { apply _. }
-    { eapply (type_delete (uninit 1) 1); solve_typing. }
+    { by eapply (type_delete (uninit 1) 1). }
     { solve_typing. }
     move=> /= _.
 
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index bc8db8522fcaf7d706d839aa9097d3f860d97fe9..a6d7c2892a58d51b5e6895b9c8fbb4357e8de56e 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -201,6 +201,16 @@ Section typing.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
   Qed.
 
+  Lemma tctx_extract_hasty_share_samelft E L p ty ty' κ T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
+                                         ((p ◁ &shr{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
   Lemma tctx_extract_hasty_reborrow E L p ty ty' κ κ' T :
     lctx_lft_incl E L κ' κ → eqtype E L ty ty' →
     tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
@@ -246,3 +256,4 @@ End typing.
 
 Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share
              tctx_extract_hasty_reborrow : lrust_typing.
+Hint Resolve tctx_extract_hasty_share_samelft | 0 : lrust_typing.