From cfd715862d7288bc78eb6c9f7540aabe482a219c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Fri, 1 May 2020 13:02:06 +0200
Subject: [PATCH] =?UTF-8?q?Add=20L=C3=B6b=20TODO?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/logrel/subtyping_rules.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 9c352cb..f9f315a 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -194,6 +194,8 @@ Section subtyping_rules.
     iApply lty_le_exist; try (iAssumption || iApply lty_le_refl).
   Qed.
 
+  (* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
+
   (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
   Lemma lty_copyable_rec C `{!Contractive C} :
     (∀ A, ▷ lty_copyable A -∗ lty_copyable (C A)) -∗ lty_copyable (lty_rec C).
-- 
GitLab