diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 3471ce8a4155a24fb5d982d0dd089d84441d8cea..3d9b2f04f5ca35ecc4a514ef19d9dc2e749f0e13 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -970,8 +970,8 @@ Section code.
       iApply type_let; [apply rc_drop_type|solve_typing|]. iIntros (drop). simpl_subst.
       iApply (type_letcall ()); [try solve_typing..|].
       { (* FIXME : solve_typing should be able to do this. *)
-        move=>ϝ' /=. replace (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
-        solve_typing. by rewrite /ty_outlives_E /= app_nil_r. }
+        move=>ϝ' /=. change (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
+        solve_typing. }
       iIntros (content). simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 35739db07f32abaf8d7a6e15bf37b21ad86800b8..9b2a19aebea0f470b0b56b88a8acd1f59d60f6e2 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -83,18 +83,21 @@ Existing Instances tyl_wf_nil tyl_wf_cons.
 Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
   match WF with
   | tyl_wf_nil => []
+  | tyl_wf_cons ty [] _ _ => ty.(ty_lfts)
   | tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
 Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
   match WF with
   | tyl_wf_nil => []
+  | tyl_wf_cons ty [] _ _ => ty.(ty_wf_E)
   | tyl_wf_cons ty tyl _ _ => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
 Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
+  | tyl_wf_cons ty [] _ _ => ty.(ty_outlives_E) κ
   | tyl_wf_cons ty tyl _ _ => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
   end.
 
@@ -103,8 +106,9 @@ Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl.(tyl_outlives_E) α).
 Proof.
-  induction WF as [|???? IH]=>/=.
+  induction WF as [|? [] ?? IH]=>/=.
   - solve_typing.
+  - intros. by eapply ty_outlives_E_elctx_sat.
   - intros. apply elctx_sat_app, IH; [eapply ty_outlives_E_elctx_sat| |]=>//;
       (etrans; [|done]); solve_typing.
 Qed.