diff --git a/theories/logrel/examples/rec_subtyping.v b/theories/logrel/examples/rec_subtyping.v
index 55655376cf1f928a49eef25902d4ad0de913c2e2..a8f277e235e78649b94d8e4801c5b81af82cabdf 100644
--- a/theories/logrel/examples/rec_subtyping.v
+++ b/theories/logrel/examples/rec_subtyping.v
@@ -44,7 +44,7 @@ Section basics.
       iApply (lty_le_trans with "H1").
       iIntros (X' Y'). iExists X', Y'. iIntros "!>!>!>".
       iApply "IH". }
-    iApply lty_le_rec.
+    iApply lty_le_rec_internal.
     iIntros (S1 S2) "#Hrec".
     iIntros (X). iExists X, lty_bool. iIntros "!> !>" (Y).
     iApply (lty_le_trans _ (<??> TY lty_bool; <!!> TY Y ⊸ lty_int;
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 46060b67a03e3ffa5d1ac6e511f4662a74a89e21..081681e4596b976f0f2f18b6a1210e5d52140007 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -41,8 +41,8 @@ Section subtyping_rules.
     - rewrite {2}/lty_rec fixpoint_unfold. iApply lty_le_refl.
   Qed.
 
-  Lemma lty_le_rec {k} (C1 C2 : lty Σ k → lty Σ k)
-        `{Contractive C1, Contractive C2} :
+  Lemma lty_le_rec_internal {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
     (∀ K1 K2, ▷ (K1 <: K2) -∗ C1 K1 <: C2 K2) -∗
     lty_rec C1 <: lty_rec C2.
   Proof.
@@ -51,6 +51,17 @@ Section subtyping_rules.
     iApply lty_le_r; [|iApply lty_bi_le_sym; iApply lty_le_rec_unfold].
     by iApply "Hle".
   Qed.
+  Lemma lty_le_rec_external {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
+    (∀ K1 K2, (K1 <: K2) → C1 K1 <: C2 K2) →
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    intros IH. rewrite /lty_rec. apply fixpoint_ind.
+    - by intros K1' K2' -> ?.
+    - exists (fixpoint C2). iApply lty_le_refl.
+    - intros K' ?. rewrite (fixpoint_unfold C2). by apply IH.
+    - apply bi.limit_preserving_entails; [done|solve_proper].
+  Qed.
 
   (** Term subtyping *)
   Lemma lty_le_any A : A <: any.