From a28b7fd808200a3e48a665662a2b7183abab6a44 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 29 May 2025 16:58:55 -0400 Subject: [PATCH] Add comments --- theories/properties.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/properties.v b/theories/properties.v index bcd72d6..c277856 100644 --- a/theories/properties.v +++ b/theories/properties.v @@ -96,4 +96,11 @@ Module Typing. - hauto lq:on ctrs:Wt use:ren_up. Qed. + (* Liftable: stable *) +(* If a well-typed term is liftable, then it should remain well-typed at the same level +if the floating variables are lifted *) + + (* Upgrade *) + (* If Γ ⊢ a ;; ℓ ∈ A, we want to lift up the levels in Γ *) + End Typing.