excerpt.v

 Fixpoint fundamental_subtype {Γ T1 i1 T2 i2} (HT: Γ ⊢ₜ T1, i1 <: T2, i2) {struct HT}:
    Γ ⊨ T1, i1 <: T2, i2
  with
  fundamental_typed {Γ e T} (HT: Γ ⊢ₜ e : T) {struct HT}:
    Γ ⊨ e : T.
  Proof.
    - iInduction HT as [] "IHT".
      + by iApply Sub_Refl.
      + by iApply Sub_Trans.
      + by iIntros "!> **".
      (* + by iApply Sub_Later.
      + by iApply Sub_Mono. *)
      + by iApply Sub_Index_Incr.
      + by iApply Sub_Top.
      + by iApply Bot_Sub.
      + iApply Sel_Sub. by unshelve iApply (fundamental_typed _ _ _ _).
      + iApply Sub_Sel. by unshelve iApply (fundamental_typed _ _ _ _).
      + by iApply Sub_TAllConCov.
      + by iApply Sub_TTMem_Variant.
    - iInduction HT as [] "IHT".
      + by iApply T_Forall_Ex.
      + by iApply T_Forall_E.
      + by iApply T_Forall_I.
      + by iApply T_Nat_I.
      + by iApply T_Var.
      + iApply T_Sub => //.
        by iApply (fundamental_subtype _ _ _ _ _ H).
      + iApply T_Vty_abs_I => //.
        by unshelve iApply (fundamental_subtype _ _ _ _ _ _).
        (* Breaks *)
        (* by unshelve iApply (fundamental_subtype _ _ _ _ _). *)
        (* Works *)
        by unshelve iApply (fundamental_subtype _ _ _ _ _ _).
  Qed.