POPL26 revised version

README.md

@@ -7,9 +7,10 @@ This repository contains the proofs for _Extensible Data Types with Ad-Hoc Polym
 The numbered theorems from the paper correspond to the following Lean theorems:
 
 - Theorem 4.1: [`TabularTypes.«F⊗⊕ω».SmallStep.local_confluence`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean)
-- Theorem 4.2: [`TabularTypes.«F⊗⊕ω».IndexedStronglyNormalizing.of_Kinding`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean)
-- Theorem 4.3: [`TabularTypes.«F⊗⊕ω».progress`](TabularTypes/F⊗⊕ω/Theorems.lean)
-- Theorem 4.4: [`TabularTypes.«F⊗⊕ω».preservation`](TabularTypes/F⊗⊕ω/Theorems.lean)
+- Theorem 4.2: [`TabularTypes.«F⊗⊕ω».StronglyNormalizing.of_Indexed`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean)
+- Theorem 4.3: [`TabularTypes.«F⊗⊕ω».IndexedStronglyNormalizing.of_Kinding`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean)
+- Theorem 4.4: [`TabularTypes.«F⊗⊕ω».progress`](TabularTypes/F⊗⊕ω/Theorems.lean)
+- Theorem 4.5: [`TabularTypes.«F⊗⊕ω».preservation`](TabularTypes/F⊗⊕ω/Theorems.lean)
 - Theorem 5.1:
   - Kinding: [`TabularTypes.TypeScheme.KindingAndElaboration.soundness`](TabularTypes/Theorems/Type/KindingAndElaboration.lean)
   - Row Equivalence: [`TabularTypes.Monotype.RowEquivalenceAndElaboration.soundness`](TabularTypes/Theorems/Type/Basic.lean)

TabularTypes/F⊗⊕ω/Semantics/Type/SmallStep.lean

@@ -173,7 +173,7 @@ inductive StronglyNormalizingToList (P : «Type» → Prop) : «Type» → Prop
   | step : (∀ B, [[ε ⊢ A -> B]] → StronglyNormalizingToList P B) → (∀ As K?, A ≠ Type.list As K?) →
       StronglyNormalizingToList P A
 
-judgement_syntax "SN" K "(" A ")" : IndexedStronglyNormalizing
+judgement_syntax "SN" K "(" A ")" : IndexedStronglyNormalizing (tex := s!"\\lottkw\{SN}_\{{K}}({A})")
 
 abbrev IndexedStronglyNormalizing : Kind → «Type» → Prop
   | [[*]], A => [[ε ⊢ A : *]] ∧ [[SN(A)]]

TabularTypes/Lemmas/Type/ToKinding.lean

@@ -31,6 +31,10 @@ theorem Monotype.RowEquivalenceAndElaboration.to_Kinding (ρee : [[Γc; Γ ⊢ 
     let ⟨_, _, _, ρ₁ke', ρ₂ke⟩ := ρ₁₂ee.to_Kinding Γcw Γwe
     cases ρ₁ke.deterministic ρ₁ke' |>.left
     exact ⟨_, _, _, ρ₀ke, ρ₂ke⟩
+  | lift I ρ₀₁ee ρ₀ke τke κ₀e _ (κ₀ := κ₀) (κ₁ := κ₁) =>
+    let ⟨_, _, _, ρ₀ke', ρ₁ke⟩ := ρ₀₁ee.to_Kinding Γcw Γwe
+    cases ρ₀ke.deterministic ρ₀ke' |>.left
+    exact ⟨_, _, _, .lift I τke κ₀e ρ₀ke, .lift I τke κ₀e ρ₁ke⟩
   | liftL _ liftke@(.lift I τ'ke κ₀e ξτke) _ (τ' := τ') (κ₁ := κ₁) =>
     let ⟨⟨_, ξke⟩, uni, ⟨_, _, _, eq, κeq, _, h, _, τke⟩⟩ := ξτke.row_inversion
     let ⟨_, κ₁e⟩ := κ₁.Elaboration_total

TabularTypes/Semantics/Type/RowEquivalenceAndElaboration.lean

@@ -3,6 +3,7 @@ import TabularTypes.Semantics.Type.KindingAndElaboration
 namespace TabularTypes
 
 open «F⊗⊕ω»
+open TabularTypes.TypeScheme
 
 judgement_syntax Γc "; " Γ " ⊢ " ρ₀ " ≡" "(" μ ") " ρ₁ " ⇝ " Fₚ ", " Fₛ : Monotype.RowEquivalenceAndElaboration (tex := s!"{Γc} \\lottsym\{;} \\, {Γ} \\, \\lottsym\{⊢} \\, {ρ₀} \\, \\rowequivsym_\{{μ}} \\, {ρ₁} \\, \\lottsym\{⇝} \\, {Fₚ} \\lottsym\{,} \\, {Fₛ}") (tex noelab := s!"{Γc} \\lottsym\{;} \\, {Γ} \\, \\lottsym\{⊢} \\, {ρ₀} \\, \\rowequivsym_\{{μ}} \\, {ρ₁}")
 
@@ -38,6 +39,16 @@ notex for noelab Fₛ := Λ a : K ↦ *. λ x : ⊕ (a$0 ⟦{</ A@i // i in [:n]
 ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── comm
 Γc; Γ ⊢ ⟨</ ξ@i ▹ τ@i // i in [:n] /> </ : κ // b />⟩ ≡(C) ⟨</ ξ@i ▹ τ@i // (tex := "i \\in p") i in p_ /> </ : κ // b />⟩ ⇝ Fₚ, Fₛ
 
+Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ', Fₛ'
+Γc; Γ ⊢ ρ₀ : R κ₀
+∀ a ∉ I, Γc; Γ, a : κ₀ ⊢ τ^a : κ₁ ⇝ A^a
+notex for noelab ⊢ κ₀ ⇝ K₀
+notex for noelab ⊢ κ₁ ⇝ K₁
+notex for noelab Fₚ := Λ a' : K₁ ↦ *. Fₚ' [λ a : K₀. a'$1 A]
+notex for noelab Fₛ := Λ a' : K₁ ↦ *. Fₛ' [λ a : K₀. a'$1 A]
+───────────────────────────────────────────────────────────────── lift (I : List TypeVarId)
+Γc; Γ ⊢ Lift (λ a : κ₀. τ) ρ₀ ≡(μ) Lift (λ a : κ₀. τ) ρ₁ ⇝ Fₚ, Fₛ
+
 Γc; Γ ⊢ Lift (λ a : κ₀. τ') ⟨</ ξ@i ▹ τ@i // i in [:n] notex /> </ : κ₀ // b notex />⟩ : R κ₁ ⇝ A
 notex for noelab ⊢ κ₁ ⇝ K
 notex for noelab Fₚ := Λ a' : K ↦ *. λ x : ⊗ (a'$0 ⟦A⟧). x$0

TabularTypes/Theorems/Type/Basic.lean

@@ -52,6 +52,11 @@ theorem symm (ρee : [[Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ, Fₛ]]) (Γcw :
     let ⟨κ', _, _, _, ρ₂ke⟩ := ρ₁₂ee.to_Kinding Γcw Γwe
     let ⟨_, κ'e⟩ := κ'.Elaboration_total
     ⟨_, _, trans ρ₂ke κ'e ρ₂₁ee ρ₁₀ee⟩
+  | lift I ρ₀₁ee ρ₀ke τke κ₀e κ₁e => by
+    let ⟨_, _, ρ₁₀ee⟩ := ρ₀₁ee.symm Γcw Γwe
+    let ⟨_, _, _, ρ₀ke', ρ₁ke⟩ := ρ₀₁ee.to_Kinding Γcw Γwe
+    cases ρ₀ke.deterministic ρ₀ke' |>.left
+    exact ⟨_, _, lift I ρ₁₀ee ρ₁ke τke κ₀e κ₁e⟩
   | liftL μ liftke κe => ⟨_, _, liftR μ liftke κe⟩
   | liftR μ liftke κe => ⟨_, _, liftL μ liftke κe⟩
 
@@ -344,6 +349,114 @@ theorem soundness (ρee : [[Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ, Fₛ]]) (
           simp only [Function.comp]
           exact .lam (.app (.var_bound Nat.one_pos) <| A'slc' i mem') <| .sumIntro .var
     ⟩
+  | lift I ρ₀₁'ee ρ₀'ke τke κ₀e κ₁e (A := A') (K₀ := K₀) =>
+    let ⟨_, _, _, ρ₀'ke', ρ₁'ke⟩ := ρ₀₁'ee.to_Kinding Γcw Γwe
+    rcases ρ₀'ke.deterministic ρ₀'ke' with ⟨κ₀eq, rfl⟩
+    cases κ₀eq
+
+    let .lift I' τke' κ₀e' ρ₀'ke'' (A := A'') := ρ₀ke
+    let .lift I'' τke'' κ₀e'' ρ₁'ke' (A := A''') := ρ₁ke
+
+    rcases ρ₀'ke.deterministic ρ₀'ke'' with ⟨κ₀eq, rfl⟩
+    cases κ₀eq
+    cases κ₀e.deterministic κ₀e'
+    cases κ₀e.deterministic κ₀e''
+
+    let ⟨a, anin⟩ := Γ.typeVarDom ++ ↑A'.freeTypeVars ++ ↑A''.freeTypeVars ++ ↑A'''.freeTypeVars ++
+      I ++ I' ++ I'' |>.exists_fresh
+    let ⟨aninΓA'A''A'''II', aninI''⟩ := List.not_mem_append'.mp anin
+    let ⟨aninΓA'A''A'''I, aninI'⟩ := List.not_mem_append'.mp aninΓA'A''A'''II'
+    let ⟨aninΓA'A''A''', aninI⟩ := List.not_mem_append'.mp aninΓA'A''A'''I
+    let ⟨aninΓA'A'', aninA'''⟩ := List.not_mem_append'.mp aninΓA'A''A'''
+    let ⟨aninΓA', aninA''⟩ := List.not_mem_append'.mp aninΓA'A''
+    let ⟨aninΓ, aninA'⟩ := List.not_mem_append'.mp aninΓA'
+
+    rcases τke a aninI |>.deterministic <| τke' a aninI' with ⟨rfl, A'eq⟩
+    cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars aninA' aninA'' A'eq
+    rcases τke a aninI |>.deterministic <| τke'' a aninI'' with ⟨_, A''eq⟩
+    cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars aninA' aninA''' A''eq
+    cases κe.deterministic κ₁e
+
+    rcases ρ₁'ke.deterministic ρ₁'ke' with ⟨_, rfl⟩
+
+    let Alc := τke a aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e
+      |>.TypeVarLocallyClosed_of.weaken (n := 1).TypeVar_open_drop Nat.one_pos
+    let B₀ki := ρ₀'ke.soundness Γcw Γwe κ₀e.row
+    let B₀lc := B₀ki.TypeVarLocallyClosed_of
+    let B₁ki := ρ₁'ke.soundness Γcw Γwe κ₀e.row
+    let B₁lc := B₁ki.TypeVarLocallyClosed_of
+    let ⟨Fₚ'ty, Fₛ'ty, Fₚ'lc, Fₛ'lc⟩ := ρ₀₁'ee.soundness Γcw Γwe ρ₀'ke ρ₁'ke κ₀e
+    let Δwf := Γwe.soundness Γcw
+    exact ⟨
+      .typeLam Γ.typeVarDom fun a' a'nin => by
+        let a'ninΔ := Γwe.TypeVarNotInDom_preservation a'nin
+        simp [Type.TypeVar_open, Term.TypeVar_open, Fₚ'lc.TypeVar_open_id, Alc.TypeVar_open_id,
+              B₀lc.TypeVar_open_id, B₁lc.TypeVar_open_id]
+        let Γa'we := Γwe.typeExt a'nin <| κ₁e.arr .star
+        let Δa'wf := Γa'we.soundness Γcw
+        let Fₚ'ty' := Fₚ'ty.weakening (Γa'we.soundness Γcw) (Δ' := .typeExt .empty ..) (Δ'' := .empty)
+          |>.typeApp (B := [[λ a : K₀. a' A']]) <| .lam ((a' :: Γ.typeVarDom) ++ ↑I) <|
+            fun a'' a''nin => by
+              simp [Type.TypeVar_open, Environment.append]
+              let ⟨a''ninΓa', a''ninI⟩ := List.not_mem_append'.mp a''nin
+              let ⟨a''ne, _⟩ := List.not_mem_cons.mp a''ninΓa'
+              refine .app (.var (.typeVarExt .head (.symm a''ne))) ?_
+              let Γa'a''we := Γa'we.typeExt a''ninΓa' κ₀e
+              exact τke _ a''ninI |>.weakening (Γ' := .typeExt .empty ..)
+                (Γ'' := .typeExt .empty ..) Γa'a''we |>.soundness Γcw Γa'a''we κ₁e
+        apply Fₚ'ty'.equiv
+        simp [Type.Type_open, B₀lc.Type_open_id, B₁lc.Type_open_id]
+        let A'ki : [[Δ ⊢ λ a : K₀. A' : K₀ ↦ K]] := .lam (Γ.typeVarDom ++ I) fun a anin => by
+          let ⟨aninΓ, aninI⟩ := List.not_mem_append'.mp anin
+          exact τke _ aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e
+        refine .arr (.prod (.symm ?_)) (.prod (.symm ?_))
+        all_goals (
+          replace A'ki := A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) Δa'wf
+          refine .trans (.listAppComp .var_free A'ki) ?_
+          refine .listApp (.lam (a' :: Δ.typeVarDom) ?_) .refl
+          intro a'' a''nin
+          simp [Type.TypeVar_open, Alc.TypeVar_open_id]
+          rw [Type.Type_open_var]
+          exact .app .refl <| .lamApp
+            (A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) (Δa'wf.typeVarExt a''nin)) <|
+            .var .head
+        ),
+      .typeLam Γ.typeVarDom fun a' a'nin => by
+        let a'ninΔ := Γwe.TypeVarNotInDom_preservation a'nin
+        simp [Type.TypeVar_open, Term.TypeVar_open, Fₛ'lc.TypeVar_open_id, Alc.TypeVar_open_id,
+              B₀lc.TypeVar_open_id, B₁lc.TypeVar_open_id]
+        let Γa'we := Γwe.typeExt a'nin <| κ₁e.arr .star
+        let Δa'wf := Γa'we.soundness Γcw
+        let Fₛ'ty' := Fₛ'ty.weakening (Γa'we.soundness Γcw) (Δ' := .typeExt .empty ..) (Δ'' := .empty)
+          |>.typeApp (B := [[λ a : K₀. a' A']]) <| .lam ((a' :: Γ.typeVarDom) ++ ↑I) <|
+            fun a'' a''nin => by
+              simp [Type.TypeVar_open, Environment.append]
+              let ⟨a''ninΓa', a''ninI⟩ := List.not_mem_append'.mp a''nin
+              let ⟨a''ne, _⟩ := List.not_mem_cons.mp a''ninΓa'
+              refine .app (.var (.typeVarExt .head (.symm a''ne))) ?_
+              let Γa'a''we := Γa'we.typeExt a''ninΓa' κ₀e
+              exact τke _ a''ninI |>.weakening (Γ' := .typeExt .empty ..)
+                (Γ'' := .typeExt .empty ..) Γa'a''we |>.soundness Γcw Γa'a''we κ₁e
+        apply Fₛ'ty'.equiv
+        simp [Type.Type_open, B₀lc.Type_open_id, B₁lc.Type_open_id]
+        let A'ki : [[Δ ⊢ λ a : K₀. A' : K₀ ↦ K]] := .lam (Γ.typeVarDom ++ I) fun a anin => by
+          let ⟨aninΓ, aninI⟩ := List.not_mem_append'.mp anin
+          exact τke _ aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e
+        refine .arr (.sum (.symm ?_)) (.sum (.symm ?_))
+        all_goals (
+          replace A'ki := A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) Δa'wf
+          refine .trans (.listAppComp .var_free A'ki) ?_
+          refine .listApp (.lam (a' :: Δ.typeVarDom) ?_) .refl
+          intro a'' a''nin
+          simp [Type.TypeVar_open, Alc.TypeVar_open_id]
+          rw [Type.Type_open_var]
+          exact .app .refl <| .lamApp
+            (A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) (Δa'wf.typeVarExt a''nin)) <|
+            .var .head
+        ),
+      .typeLam <| .typeApp Fₚ'lc.weaken <| .lam <| .app (.var_bound Nat.le.refl) Alc.weaken,
+      .typeLam <| .typeApp Fₛ'lc.weaken <| .lam <| .app (.var_bound Nat.le.refl) Alc.weaken
+    ⟩
   | liftL μ liftke@(.lift I τ'ke κ₀e ξτke) κe' (τ := τ) (τ' := τ') =>
     rename_i A' _ _
     let ⟨κeq, Aeq⟩ := liftke.deterministic ρ₀ke

tex/TabularTypes/Monotype/RowEquivalenceAndElaboration.tex

@@ -23,6 +23,16 @@
 \lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \targetpre K \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre \lottsym{⊕} \, \targetpre \lottsym{(} \targetpre \targetpre \targetpre a \targetpost \targetpost \, \lottsym{⟦} \targetpre \lottsym{\{} \lottsepbycomprehensionpatcollection{\targetpre A_{i} \targetpost}{i}{[:n]} \lottsym{\}} \targetpost \lottsym{⟧} \targetpost \lottsym{)} \targetpost \targetpost \lottsym{.} \, \targetpre \lottkw{case} \, \targetpre \targetpre x \targetpost \targetpost \, \lottsym{\{} \lottsepbycomprehensioncustom{\targetpre \lottsym{λ} \, \targetpre x' \targetpost \, \lottsym{:} \, \targetpre \targetpre \targetpre a \targetpost \targetpost \, \targetpre A_{i} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{ι}_{j} \, \targetpre \targetpre x' \targetpost \targetpost \targetpost \targetpost}{i \in [:n], j \in p'} \lottsym{\}} \targetpost \targetpost \targetpost}
 }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩} \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost}
 \lottinferencerulesep
+\lottinferencerule{lift}{
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ' \targetpost \lottsym{,} \, \targetpre Fₛ' \targetpost}\\
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁ \, \lottsym{⇝} \, \targetpre \targetpre A \targetpost \targetpost}\\
+\lotthypothesis{\lottsym{⊢} \, κ₀ \, \lottsym{⇝} \, \targetpre K₀ \targetpost}\\
+\lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K₁ \targetpost}\\
+\lottlet{\targetpre Fₚ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₚ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost}\\
+\lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₛ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost}
+}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost}
+\lottinferencerulesep
 \lottinferencerule{liftL}{
 \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁} \, \lottsym{⇝} \, \targetpre A \targetpost}\\
 \lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K \targetpost}\\

tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelab.tex

@@ -14,6 +14,12 @@
 \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ}}
 }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩}}
 \lottinferencerulesep
+\lottinferencerule{lift}{
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁}\\
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\
+\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁}
+}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁}
+\lottinferencerulesep
 \lottinferencerule{liftL}{
 \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁}}
 }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \rowequivsym_{μ} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ'\left[τ_{i}/a\right]} \lottsym{⟩}}