Added a lemma for sharing without reborrowing.

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=> /= _.
 

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.