diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index f864d2e3d1eb11c309917fa590ef5823b0dd3eac..2dc0f77abe2ae0ccf21870efa968d490d7811bf4 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -99,6 +99,10 @@ Section subtype.
     iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
   Qed.
 
+  Lemma lty_exist_le_elim C B :
+    ⊢ (C B) <: (∃ A, C A).
+  Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
+
   Lemma lty_rec_le_1 (C : lty Σ → lty Σ) `{!Contractive C} :
     ⊢ lty_rec C <: C (lty_rec C).
   Proof.