diff --git "a/TabularTypeInterpreter/F\342\212\227\342\212\225\317\211/Lemmas/Term.lean" "b/TabularTypeInterpreter/F\342\212\227\342\212\225\317\211/Lemmas/Term.lean" index e7504c9..b59fb13 100644 --- "a/TabularTypeInterpreter/F\342\212\227\342\212\225\317\211/Lemmas/Term.lean" +++ "b/TabularTypeInterpreter/F\342\212\227\342\212\225\317\211/Lemmas/Term.lean" @@ -163,6 +163,12 @@ where of_eq {E m n} (Elc : TermVarLocallyClosed E m) (eq : m = n) : E.TermVarLocallyClosed n := by rwa [eq] at Elc +theorem TermVar_open_TermVar_close_id + : TermVarLocallyClosed E n → (TermVar_close E x n).TermVar_open x n = E := by + induction E using rec_uniform generalizing n <;> aesop + (add simp [TermVar_open, TermVar_close], 40% cases TermVarLocallyClosed, + safe List.map_eq_id_of_eq_id_of_mem) + end TermVarLocallyClosed theorem Term_open_TermVar_open_comm : TermVarLocallyClosed F m → m ≠ n → diff --git a/TabularTypeInterpreter/Lemmas/Term.lean b/TabularTypeInterpreter/Lemmas/Term.lean new file mode 100644 index 0000000..337deb1 --- /dev/null +++ b/TabularTypeInterpreter/Lemmas/Term.lean @@ -0,0 +1,93 @@ +import TabularTypeInterpreter.Lemmas.Type.Basic +import TabularTypeInterpreter.Semantics.Term + +namespace TabularTypeInterpreter + +open Std + +namespace Term + +namespace TermVarLocallyClosed + +theorem weakening : TermVarLocallyClosed M m → TermVarLocallyClosed M (m + n) := sorry + +theorem TermVar_open_id : TermVarLocallyClosed M n → TermVar_open M x n = M := sorry + +end TermVarLocallyClosed + +namespace TypingAndElaboration + +theorem TermVarLocallyClosed_of (Mte : [[Γᵢ; Γc; Γ ⊢ M : σ ⇝ E]]) : M.TermVarLocallyClosed := sorry + +theorem weakening (Mte : [[Γᵢ; Γc; Γ, Γ'' ⊢ M : σ ⇝ E]]) (Γwe : [[Γc ⊢ Γ, Γ', Γ'' ⇝ Δ]]) + : [[Γᵢ; Γc; Γ, Γ', Γ'' ⊢ M : σ ⇝ E]] := by + sorry + -- generalize Γ'''eq : [[Γ, Γ'']] = Γ''' at Mte + -- induction Mte generalizing Δ Γ'' <;> try cases Γ'''eq + -- · case var xσinΓ => + -- sorry + -- · case lam I _ τ₀ke ih => + -- let τ₀ke' := τ₀ke.weakening Γwe + -- apply lam (I ++ [[Γ, Γ', Γ'']].termVarDom) _ τ₀ke' + -- intro x xnin + -- let ⟨xninI, xninΓ⟩ := List.not_mem_append'.mp xnin + -- let Γxwe := Γwe.termExt xninΓ τ₀ke' + -- rw [← TypeEnvironment.append, ← TypeEnvironment.append] at Γxwe ⊢ + -- exact ih x xninI Γxwe rfl + -- · case app _ _ M'ih Nih => exact app (M'ih Γwe rfl) (Nih Γwe rfl) + -- · case qualI I ψke _ ih => + -- let ψke' := ψke.weakening Γwe + -- apply qualI (I ++ [[Γ, Γ', Γ'']].termVarDom) ψke' + -- intro x xnin + -- let ⟨xninI, xninΓ⟩ := List.not_mem_append'.mp xnin + -- let Γxwe := Γwe.constrExt xninΓ ψke' + -- rw [← TypeEnvironment.append, ← TypeEnvironment.append] at Γxwe ⊢ + -- exact ih x xninI Γxwe rfl + -- · case qualE ψce _ ih => + -- apply qualE <| ψce.weakening + +theorem singleton_prod (Mte : [[Γᵢ; Γc; Γ ⊢ M : ⌊ξ⌋ ⇝ F]]) (Nte : [[Γᵢ; Γc; Γ ⊢ «N» : τ ⇝ E]]) + (ξke : [[Γc; Γ ⊢ ξ : L ⇝ A₀]]) (τke : [[Γc; Γ ⊢ τ : * ⇝ A₁]]) (μke : [[Γc; Γ ⊢ μ : U ⇝ B]]) + : [[Γᵢ; Γc; Γ ⊢ {M ▹ «N»} : Π(μ) ⟨ξ ▹ τ⟩ ⇝ ⦅λ x : ⊗ {A₁}. x$0⦆ (E)]] := by + let prodte := prod (by + intro _ mem + cases Nat.eq_of_le_of_lt_succ mem.lower mem.upper + exact Mte + ) (by rw [Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_same_eq_nil]; exact .var) (by + intro _ mem + cases Nat.eq_of_le_of_lt_succ mem.lower mem.upper + exact Nte + ) (.inl nofun) (b := false) (n := 1) (Γᵢ := Γᵢ) (Γc := Γc) (Γ := Γ) + (M := fun _ => M) («N» := fun _ => «N») (ξ := fun _ => ξ) + (τ := fun _ => τ) (E := fun _ => E) (F := fun _ => F) + rw [Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_eq_cons_of_lt Nat.zero_lt_one, + Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_same_eq_nil, Range.map_same_eq_nil, + Range.map_same_eq_nil, Option.someIf, if_neg nofun] at prodte + simp only at prodte + let prodte' := prodte.sub <| .decay (.prod .comm <| .singleton_row ξke τke) μke .N + exact prodte' + +instance : Inhabited Term where + default := .prod [] +in +instance __ : Inhabited Monotype where + default := .row [] none +in +instance : Inhabited «F⊗⊕ω».Term where + default := .prodIntro [] +in +theorem unit (μke : [[Γc; Γ ⊢ μ : U ⇝ B]]) + : [[Γᵢ; Γc; Γ ⊢ {} : Π(μ) ⟨ : * ⟩ ⇝ ⦅λ x : ⊗ { }. x$0⦆ ()]] := by + let prodte := prod nofun (.concrete nofun) nofun (.inr rfl) (n := 0) (Γᵢ := Γᵢ) (Γc := Γc) (Γ := Γ) + (M := fun _ => default) («N» := fun _ => default) (ξ := fun _ => .label .zero) + (τ := fun _ => default) (E := fun _ => default) (F := fun _ => default) + rw [Range.map_same_eq_nil, Range.map_same_eq_nil, Range.map_same_eq_nil, Option.someIf, + if_pos rfl] at prodte + let prodte' := prodte.sub <| .decay (.prod .comm .empty_row) μke .N + exact prodte' + +end TypingAndElaboration + +end Term + +end TabularTypeInterpreter diff --git a/TabularTypeInterpreter/Semantics/Term.lean b/TabularTypeInterpreter/Semantics/Term.lean index 2e67021..a51f26a 100644 --- a/TabularTypeInterpreter/Semantics/Term.lean +++ b/TabularTypeInterpreter/Semantics/Term.lean @@ -40,8 +40,8 @@ x : σ ∈ Γ Γᵢ; Γc; Γ ⊢ M «N» : τ₁ ⇝ F E Γc; Γ ⊢ ψ : C ⇝ A -∀ x ∉ I, Γᵢ; Γc; Γ, ψ ⇝ x ⊢ M^x : γ ⇝ E^x -───────────────────────────────────────── qualI (I : List TermVarId) +∀ x ∉ I, Γᵢ; Γc; Γ, ψ ⇝ x ⊢ M : γ ⇝ E^x +─────────────────────────────────────── qualI (I : List TermVarId) Γᵢ; Γc; Γ ⊢ M : ψ ⇒ γ ⇝ λ x : A. E Γᵢ; Γc; Γ ⊨ ψ ⇝ E @@ -118,10 +118,10 @@ notex n ≠ 0 ∨ b ──────────────────────────────────────────────────────────────────────── elim Γᵢ; Γc; Γ ⊢ M ▿ «N» : (Σ(μ) ρ₂) → τ ⇝ ⦅⦅π 1 F⦆ [λ a : *. a$0] [A] E₀⦆ E₁ -Γᵢ; Γc; Γ ⊢ M : τ₀ ⇝ E -Γc; Γ ⊢ τ₀ <: τ₁ ⇝ F +Γᵢ; Γc; Γ ⊢ M : σ₀ ⇝ E +Γc; Γ ⊢ σ₀ <: σ₁ ⇝ F ──────────────────────── sub -Γᵢ; Γc; Γ ⊢ M : τ₁ ⇝ F E +Γᵢ; Γc; Γ ⊢ M : σ₁ ⇝ F E ( ⇒ TC a : κ) ↦ m : σ ⇝ A ∈ Γc Γᵢ; Γc; Γ ⊨ TC τ ⇝ E diff --git a/TabularTypeInterpreter/Theorems.lean b/TabularTypeInterpreter/Theorems.lean index d78a264..4974d6d 100644 --- a/TabularTypeInterpreter/Theorems.lean +++ b/TabularTypeInterpreter/Theorems.lean @@ -1,3 +1,4 @@ +import TabularTypeInterpreter.Theorems.GenericEmulation import TabularTypeInterpreter.Theorems.Kind import TabularTypeInterpreter.Theorems.Program import TabularTypeInterpreter.Theorems.Term diff --git a/TabularTypeInterpreter/Theorems/GenericEmulation.lean b/TabularTypeInterpreter/Theorems/GenericEmulation.lean new file mode 100644 index 0000000..659ce9a --- /dev/null +++ b/TabularTypeInterpreter/Theorems/GenericEmulation.lean @@ -0,0 +1,619 @@ +import TabularTypeInterpreter.Lemmas.Term +import TabularTypeInterpreter.Semantics.Term +import TabularTypeInterpreter.Theorems.Term + +namespace TabularTypeInterpreter + +open «F⊗⊕ω» +open Std +open Term +open Term.TypingAndElaboration +open TypeScheme +open Monotype + +-- instance : Inhabited Monotype where +-- default := .row [] none +-- in +-- theorem ana_emulation (ρke : [[Γc; Γ ⊢ ρ : R κ ⇝ A₀]]) (ϕke : [[Γc; Γ ⊢ ϕ : κ ↦ * ⇝ A₁]]) +-- (μke : [[Γc; Γ ⊢ μ : U ⇝ B₁]]) (τke : [[Γc; Γ ⊢ τ : * ⇝ A₂]]) +-- (Mte : [[Γᵢ; Γc; Γ ⊢ M : ∀ aₗ : L. ∀ aₜ : κ. ∀ aₚ : R κ. ∀ aᵢ : R κ. ∀ aₙ : R κ. aₚ$2 ⊙(N) ⟨aₗ$4 ▹ aₜ$3⟩ ~ aᵢ$1 ⇒ aᵢ$1 ⊙(N) aₙ$0 ~ ρ ⇒ ⌊aₗ$4⌋ → (ϕ aₜ$3) → τ ⇝ E]]) +-- (indce : [[Γᵢ; Γc; Γ ⊨ Ind ρ ⇝ F]]) (Γᵢw : [[Γc ⊢ Γᵢ]]) (Γcw : [[⊢c Γc]]) (Γwe : [[Γc ⊢ Γ ⇝ Δ]]) +-- : ∃ F, [[Γᵢ; Γc; Γ ⊢ ind (λ a : R κ. (Σ(μ) (Lift (λ a' : κ. ϕ a'$0) a$0)) → τ) ρ; (λ xₗ. λ xₐ. xₐ$0 ▿ (λ x. (M xₗ$2) x$0/xₗ$2)); (λ x. x$0) : (Σ(μ) (Lift (λ a : κ. ϕ a$0) ρ)) → τ ⇝ F]] := by +-- let ⟨K, κe⟩ := κ.Elaboration_total +-- apply Exists.intro _ +-- let Mlc := Mte.TermVarLocallyClosed_of +-- let .qual (.mono ρlc) := ρke.TypeVarLocallyClosed_of +-- let .qual (.mono τlc) := τke.TypeVarLocallyClosed_of +-- let .qual (.mono ϕlc) := ϕke.TypeVarLocallyClosed_of +-- let Elc := Mte.soundness (by +-- apply KindingAndElaboration.scheme Γ.typeVarDom +-- intro aₗ aₗnin +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open] +-- rw [ρlc.weakening (n := 4).TypeVar_open_id, τlc.weakening (n := 4).TypeVar_open_id, +-- ϕlc.weakening (n := 4).TypeVar_open_id] +-- apply defer_equality' +-- · apply KindingAndElaboration.scheme <| aₗ :: Γ.typeVarDom +-- intro aₜ aₜnin +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open] +-- rw [ρlc.weakening (n := 3).TypeVar_open_id, τlc.weakening (n := 3).TypeVar_open_id, +-- ϕlc.weakening (n := 3).TypeVar_open_id] +-- apply defer_equality' +-- · apply KindingAndElaboration.scheme <| aₜ :: aₗ :: Γ.typeVarDom +-- intro aₚ aₚnin +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open] +-- rw [ρlc.weakening (n := 2).TypeVar_open_id, τlc.weakening (n := 2).TypeVar_open_id, +-- ϕlc.weakening (n := 2).TypeVar_open_id] +-- apply defer_equality' +-- · apply KindingAndElaboration.scheme <| aₚ :: aₜ :: aₗ :: Γ.typeVarDom +-- intro aᵢ aᵢnin +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open] +-- rw [ρlc.weakening (n := 1).TypeVar_open_id, τlc.weakening (n := 1).TypeVar_open_id, +-- ϕlc.weakening (n := 1).TypeVar_open_id] +-- apply defer_equality' +-- · apply KindingAndElaboration.scheme <| aᵢ :: aₚ :: aₜ :: aₗ :: Γ.typeVarDom +-- intro aₙ aₙnin +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open] +-- rw [ρlc.TypeVar_open_id, τlc.TypeVar_open_id, ϕlc.TypeVar_open_id] +-- apply defer_equality' +-- · let Γawe := Γwe.typeExt aₗnin .label |>.typeExt aₜnin κe |>.typeExt aₚnin κe.row +-- |>.typeExt aᵢnin κe.row |>.typeExt aₙnin κe.row +-- apply KindingAndElaboration.qual <| .concat .comm +-- (.var (.typeExt sorry (.typeExt sorry .head))) +-- (.singleton_row +-- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) +-- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) +-- (.var (.typeExt sorry .head)) κe +-- (.contain .comm (.var (.typeExt sorry (.typeExt sorry .head))) +-- (.var (.typeExt sorry .head)) κe) +-- (.contain .comm +-- (.singleton_row +-- (.var (.typeExt sorry (.typeExt sorry +-- (.typeExt sorry (.typeExt sorry .head))))) +-- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) +-- (.var (.typeExt sorry .head)) κe) +-- · let ρke' := ρke.weakening Γawe (Γ'' := .empty) +-- (Γ' := .typeExt (.typeExt (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) +-- apply KindingAndElaboration.qual <| .concat .comm (.var (.typeExt sorry .head)) +-- (.var .head) ρke' κe (.contain .comm (.var (.typeExt sorry .head)) ρke' κe) +-- (.contain .comm (.var .head) ρke' κe) +-- · apply KindingAndElaboration.arr <| .floor <| .var <| .typeExt sorry <| +-- .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head +-- let ϕke' := ϕke.weakening Γawe (Γ'' := .empty) (Γ' := .typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) +-- let τke' := τke.weakening Γawe (Γ'' := .empty) (Γ' := .typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) +-- exact ϕke'.app (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head)))) +-- |>.arr τke' +-- · exact .star +-- · exact .star + + + + +-- -- (.singleton_row +-- -- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) +-- -- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head)))) +-- -- (.var (.typeExt sorry .head)) κe +-- -- (.contain .comm (.var (.typeExt sorry (.typeExt sorry .head))) +-- -- (.var (.typeExt sorry .head)) κe) +-- -- (.contain .comm +-- -- (.singleton_row +-- -- (.var (.typeExt sorry (.typeExt sorry +-- -- (.typeExt sorry (.typeExt sorry .head))))) +-- -- (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) +-- -- (.var (.typeExt sorry .head)) κe) + +-- ) Γᵢw Γcw Γwe |>.TermVarLocallyClosed_of +-- let .qual (.mono μlc) := μke.TypeVarLocallyClosed_of +-- let A₁lc := ϕke.soundness Γcw Γwe (.arr κe .star) |>.TypeVarLocallyClosed_of +-- let A₂lc := τke.soundness Γcw Γwe .star |>.TypeVarLocallyClosed_of +-- have : Monotype.arr (.prodOrSum .sum μ (.lift (.mk κ (.app ϕ (.var (.bound 0)))) ρ)) τ = +-- .Monotype_open (.arr (.prodOrSum .sum μ (.lift (.mk κ (.app ϕ (.var (.bound 0)))) (.var (.bound 0)))) τ) ρ := by +-- simp [Monotype.Monotype_open, TypeLambda.Monotype_open] +-- exact ⟨ +-- ⟨μlc.Monotype_open_id.symm, ϕlc.weakening (n := 1).Monotype_open_id.symm⟩, +-- τlc.Monotype_open_id.symm +-- ⟩ +-- rw [this] +-- apply «ind» Γ.typeVarDom Γ.typeVarDom ρke ?ϕappake κe ?M'te ?Nte indce +-- case ϕappake => +-- intro a anin +-- simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open] +-- rw [μlc.TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, τlc.TypeVar_open_id] +-- let Γawe := Γwe.typeExt anin κe.row +-- let μke' := μke.weakening Γawe (Γ' := .typeExt .empty ..) (Γ'' := .empty) +-- let sumke := KindingAndElaboration.sum μke' <| .lift [[Γ, a : R κ]].typeVarDom (by +-- intro a' a'nin +-- let Γaa'we := Γawe.typeExt a'nin κe +-- let ϕke' := ϕke.weakening Γaa'we (Γ' := .typeExt (.typeExt .empty ..) ..) (Γ'' := .empty) +-- let ϕappa'ke := ϕke'.app <| .var .head +-- have : ϕ.app (.var (.free a')) = .TypeVar_open (ϕ.app (.var (.bound 0))) a' := by +-- rw [Monotype.TypeVar_open, Monotype.TypeVar_open, if_pos rfl, ϕlc.TypeVar_open_id] +-- rw [this] at ϕappa'ke +-- have : A₁.app (.var (.free a')) = .TypeVar_open (A₁.app (.var (.bound 0))) a' := by +-- rw [Type.TypeVar_open, Type.TypeVar_open, if_pos rfl, A₁lc.TypeVar_open_id] +-- rw [this] at ϕappa'ke +-- exact ϕappa'ke +-- ) κe (.var .head) +-- let sumarrke := sumke.arr <| τke.weakening Γawe (Γ' := .typeExt .empty ..) +-- have : ((«Type».lam K (A₁.app (.var (.bound 0)))).listApp (.var (.free a))).sum.arr A₂ = +-- .TypeVar_open +-- (((«Type».lam K (A₁.app (.var (.bound 0)))).listApp (.var (.bound 0))).sum.arr A₂) a := by +-- simp [Type.TypeVar_open] +-- rw [A₁lc.weaken (n := 1).TypeVar_open_id, A₂lc.TypeVar_open_id] +-- exact ⟨rfl, rfl⟩ +-- rw [this] at sumarrke +-- exact sumarrke +-- case M'te => +-- intro aₗ aₗnin +-- intro aₜ aₜnin +-- let aₗneaₜ := List.ne_of_not_mem_cons aₜnin +-- intro aₚ aₚnin +-- let aₜneaₚ := List.ne_of_not_mem_cons aₚnin +-- let aₗneaₚ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons aₚnin +-- intro aᵢ aᵢnin +-- let aₚneaᵢ := List.ne_of_not_mem_cons aᵢnin +-- let aₜneaᵢ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons aᵢnin +-- let aₗneaᵢ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons <| +-- List.not_mem_of_not_mem_cons aᵢnin +-- intro aₙ aₙnin +-- let aᵢneaₙ := List.ne_of_not_mem_cons aₙnin +-- let aₚneaₙ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons aₙnin +-- let aₜneaₙ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons <| +-- List.not_mem_of_not_mem_cons aₙnin +-- let aₗneaₙ := List.ne_of_not_mem_cons <| List.not_mem_of_not_mem_cons <| +-- List.not_mem_of_not_mem_cons <| List.not_mem_of_not_mem_cons aₙnin +-- symm at aₗneaₜ aₜneaₚ aₗneaₚ aₚneaᵢ aₜneaᵢ aₗneaᵢ aᵢneaₙ aₚneaₙ aₜneaₙ aₗneaₙ +-- simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, +-- TypeLambda.TypeVar_open] +-- rw [μlc.TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, τlc.TypeVar_open_id, +-- μlc.TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, τlc.TypeVar_open_id] +-- let Γawe := Γwe.typeExt aₗnin .label |>.typeExt aₜnin κe |>.typeExt aₚnin κe.row +-- |>.typeExt aᵢnin κe.row |>.typeExt aₙnin κe.row +-- let Mte' := Mte.weakening Γawe (Γ'' := .empty) +-- (Γ' := .typeExt (.typeExt (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) +-- let Mte'' := Mte'.schemeE <| .var <| .typeExt aₗneaₙ <| .typeExt aₗneaᵢ <| .typeExt aₗneaₚ <| +-- .typeExt aₗneaₜ .head +-- let Mte''' := Mte''.schemeE <| .var <| .typeExt aₜneaₙ <| .typeExt aₜneaᵢ <| +-- .typeExt aₜneaₚ .head +-- let Mte'''' := Mte'''.schemeE <| .var <| .typeExt aₚneaₙ <| .typeExt aₚneaᵢ .head +-- let Mte''''' := Mte''''.schemeE <| .var <| .typeExt aᵢneaₙ .head +-- let Mte'''''' := Mte'''''.schemeE <| .var .head +-- simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, +-- Monotype.Monotype_open] at Mte'''''' +-- rw [ρlc.weakening (n := 4).Monotype_open_id, ρlc.weakening (n := 3).Monotype_open_id, +-- ρlc.weakening (n := 2).Monotype_open_id, ρlc.weakening (n := 1).Monotype_open_id, +-- ρlc.Monotype_open_id, ϕlc.weakening (n := 4).Monotype_open_id, +-- ϕlc.weakening (n := 3).Monotype_open_id, ϕlc.weakening (n := 2).Monotype_open_id, +-- ϕlc.weakening (n := 1).Monotype_open_id, ϕlc.Monotype_open_id, +-- τlc.weakening (n := 4).Monotype_open_id, τlc.weakening (n := 3).Monotype_open_id, +-- τlc.weakening (n := 2).Monotype_open_id, τlc.weakening (n := 1).Monotype_open_id, +-- τlc.Monotype_open_id] at Mte'''''' +-- let ⟨_, .qual ψ₀ke (.qual ψ₁ke _ _) _⟩ := Mte''''''.to_Kinding Γᵢw Γcw Γawe +-- apply defer_equality +-- · apply qualI Γ.termVarDom ψ₀ke +-- intro xₙₗ xₙₗnin +-- let Γaxₙₗwe := Γawe.constrExt xₙₗnin ψ₀ke +-- apply defer_equality +-- · let ψ₁ke' := ψ₁ke.weakening Γaxₙₗwe (Γ' := .constrExt .empty ..) (Γ'' := .empty) +-- apply qualI (xₙₗ :: Γ.termVarDom) ψ₁ke' +-- intro xₙᵣ xₙᵣnin +-- let Γaxₙₗᵣwe := Γaxₙₗwe.constrExt xₙᵣnin ψ₁ke' +-- apply defer_equality +-- · apply lam (xₙᵣ :: xₙₗ :: Γ.termVarDom) ?bodyke <| .floor <| .var <| .constrExt <| .constrExt <| +-- .typeExt aₗneaₙ <| .typeExt aₗneaᵢ <| .typeExt aₗneaₚ <| .typeExt aₗneaₜ .head +-- case bodyke => +-- intro xₗ xₗnin +-- let Γaxₙₗᵣxₗwe := Γaxₙₗᵣwe.termExt xₗnin <| .floor <| .var <| .constrExt <| .constrExt <| +-- .typeExt aₗneaₙ <| .typeExt aₗneaᵢ <| .typeExt aₗneaₚ <| .typeExt aₗneaₜ .head +-- simp [Term.TermVar_open] +-- rw [Mlc.weakening (n := 2).TermVar_open_id] +-- apply defer_equality +-- · let μke' := μke.weakening Γaxₙₗᵣxₗwe (Γ'' := .empty) +-- (Γ' := .termExt (.constrExt (.constrExt (.typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) ..) ..) +-- let τke' := τke.weakening Γaxₙₗᵣxₗwe (Γ'' := .empty) +-- (Γ' := .termExt (.constrExt (.constrExt (.typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) ..) ..) +-- let arrke := KindingAndElaboration.arr (.sum μke' <| .lift +-- (aₙ :: aᵢ :: aₚ :: aₜ :: aₗ :: Γ.typeVarDom) (by +-- intro a anin +-- let Γaxₙₗᵣxₗawe := Γaxₙₗᵣxₗwe.typeExt anin κe +-- let ϕke' := ϕke.weakening Γaxₙₗᵣxₗawe (Γ'' := .empty) +-- (Γ' := .typeExt (.termExt (.constrExt (.constrExt (.typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) ..) ..) ..) +-- let ϕappake := ϕke'.app <| .var .head +-- have : ϕ.app (.var (.free a)) = .TypeVar_open (ϕ.app (.var (.bound 0))) a := by +-- simp [Monotype.TypeVar_open] +-- rw [ϕlc.TypeVar_open_id] +-- rw [this] at ϕappake +-- have : A₁.app (.var (.free a)) = .TypeVar_open (A₁.app (.var (.bound 0))) a := by +-- simp [Type.TypeVar_open] +-- rw [A₁lc.TypeVar_open_id] +-- rw [this] at ϕappake +-- exact ϕappake +-- ) κe (.var (.termExt (.constrExt (.constrExt (.typeExt sorry (.typeExt sorry .head))))))) τke' +-- apply lam (xₗ :: xₙᵣ :: xₙₗ :: Γ.termVarDom) ?elimte arrke +-- case elimte => +-- intro xₐ xₐnin +-- let Γaxₙₗᵣxₗₐwe := Γaxₙₗᵣxₗwe.termExt xₐnin arrke +-- simp [Term.TermVar_open] +-- rw [Mlc.weakening (n := 1).TermVar_open_id] +-- apply defer_equality +-- · apply elim <| .var .head +-- let μke'' := μke'.weakening Γaxₙₗᵣxₗₐwe (Γ' := .termExt .empty ..) (Γ'' := .empty) +-- let ϕke' := ϕke.weakening Γaxₙₗᵣxₗₐwe (Γ'' := .empty) +-- (Γ' := .termExt (.termExt (.constrExt (.constrExt (.typeExt (.typeExt +-- (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) ..) ..) ..) +-- let sumke := KindingAndElaboration.sum μke'' <| .singleton_row +-- (.var (.termExt (.termExt (.constrExt (.constrExt (.typeExt sorry +-- (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))))))) <| +-- ϕke'.app <| .var <| .termExt <| .termExt <| .constrExt <| .constrExt <| .typeExt sorry <| +-- .typeExt sorry <| .typeExt sorry .head +-- apply lam (xₐ :: xₗ :: xₙᵣ :: xₙₗ :: Γ.termVarDom) ?appke sumke +-- case appke => +-- intro x xnin +-- let Γaxₙₗᵣxₗₐxwe := Γaxₙₗᵣxₗₐwe.termExt xnin sumke +-- simp [Term.TermVar_open] +-- rw [Mlc.TermVar_open_id] +-- apply defer_equality +-- · apply TypingAndElaboration.app (.app _ (.var (.termExt sorry (.termExt sorry .head)))) +-- · apply unlabelSum (.var .head) (.var (.termExt sorry (.termExt sorry .head))) +-- let ϕke'' := ϕke'.weakening Γaxₙₗᵣxₗₐxwe (Γ' := .termExt .empty ..) (Γ'' := .empty) +-- exact ϕke''.app <| .var <| .termExt <| .termExt <| .termExt <| .constrExt <| .constrExt <| +-- .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head +-- swap +-- · let Mte''''''' := Mte''''''.weakening Γaxₙₗᵣxₗₐxwe (Γ'' := .empty) +-- (Γ' := .termExt (.termExt (.termExt (.constrExt (.constrExt .empty ..) ..) ..) ..) ..) +-- let Mte'''''''' := Mte'''''''.qualE <| .local <| .termExt sorry <| .termExt sorry <| +-- .termExt sorry <| .constrExt sorry .head +-- exact Mte''''''''.qualE <| .local <| .termExt sorry <| .termExt sorry <| +-- .termExt sorry .head +-- · show _ = «F⊗⊕ω».Term.TermVar_open (((((((((E.typeApp («Type».var («F⊗⊕ω».TypeVar.free aₗ))).typeApp («Type».var («F⊗⊕ω».TypeVar.free aₜ))).typeApp («Type».var («F⊗⊕ω».TypeVar.free aₚ))).typeApp («Type».var («F⊗⊕ω».TypeVar.free aᵢ))).typeApp («Type».var («F⊗⊕ω».TypeVar.free aₙ))).app («F⊗⊕ω».Term.var («F⊗⊕ω».TermVar.free xₙₗ))).app («F⊗⊕ω».Term.var («F⊗⊕ω».TermVar.free xₙᵣ))).app («F⊗⊕ω».Term.var («F⊗⊕ω».TermVar.free xₗ))).app ((«F⊗⊕ω».Term.var (.bound 0)).sumElim [«F⊗⊕ω».Term.lam (A₁.app («Type».var («F⊗⊕ω».TypeVar.free aₜ))) («F⊗⊕ω».Term.var (.bound 0))])) x +-- simp [«F⊗⊕ω».Term.TermVar_open] +-- · sorry +-- · sorry +-- · sorry +-- · sorry +-- · sorry +-- case Nte => +-- simp [Monotype.Monotype_open, TypeLambda.Monotype_open] +-- rw [μlc.Monotype_open_id, ϕlc.weakening (n := 1).Monotype_open_id, τlc.Monotype_open_id] +-- let sumke : [[Γc; Γ ⊢ Σ(μ) (Lift (λ a : κ. ϕ a$0) ⟨ : κ ⟩) : * ⇝ ⊕ (λ a : K. A₁ a$0) ⟦{ }⟧]] := by +-- apply KindingAndElaboration.sum μke +-- apply KindingAndElaboration.lift Γ.typeVarDom +-- · intro a anin +-- let Γawe := Γwe.typeExt anin κe +-- rw [Monotype.TypeVar_open, Monotype.TypeVar_open, if_pos rfl, ϕlc.TypeVar_open_id] +-- let ϕappa := ϕke.weakening Γawe (Γ' := .typeExt .empty ..) (Γ'' := .empty).app (.var .head) +-- simp [Type.TypeVar_open] +-- rw [A₁lc.TypeVar_open_id] +-- exact ϕappa +-- · exact κe +-- · exact .empty_row +-- apply lam Γ.termVarDom +-- · intro x xnin +-- rw [Term.TermVar_open, if_pos rfl] +-- let Γxwe := Γwe.termExt xnin sumke +-- let xke := var .head (Γᵢ := Γᵢ) (Γc := Γc) (Γ := Γ.termExt ..) (x := x) +-- (σ := qual <| .mono <| .prodOrSum .sum μ +-- (.lift (.mk κ (ϕ.app (.var (.bound 0)))) (.row [] (some κ)))) +-- let τke' := τke.weakening Γxwe (Γ' := .termExt .empty ..) (Γ'' := .empty) +-- let xke' := xke.sub (σ₁ := qual (.mono τ)) <| by +-- let sumke' := sumke.weakening Γxwe (Γ' := .termExt .empty ..) (Γ'' := .empty) +-- apply SubtypingAndElaboration.trans sumke' _ <| .never τke' +-- swap +-- let μke' := μke.weakening Γxwe (Γ' := .termExt .empty ..) (Γ'' := .empty) +-- apply SubtypingAndElaboration.trans sumke' _ <| .decay (.sum μke' .empty_row) .comm .C +-- swap +-- apply SubtypingAndElaboration.sumRow ?ee sumke' +-- case ee => +-- let ξ (i : Nat) : Monotype := default +-- let τ' (i : Nat) : Monotype := default +-- rw [← Range.map_get!_eq (as := []), List.length_nil, ← Option.someIf_true, +-- ← Option.someIf_true, Range.map_eq_of_eq_of_mem'' (by +-- intro i mem +-- show _ = (ξ i, τ' i) +-- nomatch mem +-- )] +-- rw (occs := .pos [3]) [Range.map_eq_of_eq_of_mem'' (by +-- intro i mem +-- show _ = (ξ i, (ϕ.app (.var (.bound 0))).Monotype_open (τ' i)) +-- nomatch mem +-- )] +-- apply RowEquivalenceAndElaboration.liftL _ _ .star +-- swap +-- rw (occs := .pos [4, 8]) [← List.length_nil] +-- rw [Range.map_eq_of_eq_of_mem'' (by +-- intro i mem +-- show _ = [].get! i +-- nomatch mem +-- ), Option.someIf_true, Range.map_get!_eq] +-- let .sum _ liftke := sumke' +-- exact liftke +-- let .app E'lc _ := xke'.soundness τke' Γᵢw Γcw Γxwe |>.TermVarLocallyClosed_of +-- have : «F⊗⊕ω».Term.var (.free x) = .TermVar_open (.var (.bound 0)) x := by +-- rw [«F⊗⊕ω».Term.TermVar_open, if_pos rfl] +-- rw [← E'lc.TermVar_open_id (x := x), this, ← «F⊗⊕ω».Term.TermVar_open] at xke' +-- exact xke' +-- · exact sumke +-- where +-- defer_equality {Γᵢ Γc Γ M σ E F} (Mte : [[Γᵢ; Γc; Γ ⊢ M : σ ⇝ E]]) (eq : E = F) +-- : TypingAndElaboration Γᵢ Γc Γ M σ F := by rwa [eq] at Mte +-- defer_equality' {Γc Γ σ κ A B} (σke : [[Γc; Γ ⊢ σ : κ ⇝ A]]) (eq : A = B) +-- : KindingAndElaboration Γc Γ σ κ B := by rwa [eq] at σke + +theorem syn_emulation (ρke : [[Γc; Γ ⊢ ρ : R κ ⇝ A₀]]) (ϕke : [[Γc; Γ ⊢ ϕ : κ ↦ * ⇝ A₁]]) + (μke : [[Γc; Γ ⊢ μ : U ⇝ B]]) + (Mte : [[Γᵢ; Γc; Γ ⊢ M : ∀ aₗ : L. ∀ aₜ : κ. ∀ aₚ : R κ. ∀ aᵢ : R κ. ∀ aₙ : R κ. aₚ$2 ⊙(N) ⟨aₗ$4 ▹ aₜ$3⟩ ~ aᵢ$1 ⇒ aᵢ$1 ⊙(N) aₙ$0 ~ ρ ⇒ ⌊aₗ$4⌋ → ϕ aₜ$3 ⇝ E]]) + (indce : [[Γᵢ; Γc; Γ ⊨ Ind ρ ⇝ F]]) (Γᵢw : [[Γc ⊢ Γᵢ]]) (Γcw : [[⊢c Γc]]) (Γwe : [[Γc ⊢ Γ ⇝ Δ]]) + : ∃ F, [[Γᵢ; Γc; Γ ⊢ ind (λ a : R κ. Π(μ) (Lift (λ a' : κ. ϕ a'$0) a$0)) ρ; (λ xₗ. λ xₐ. xₐ$0 ++ {xₗ$1 ▹ M xₗ$1}); {} : Π(μ) (Lift (λ a : κ. ϕ a$0) ρ) ⇝ F]] := by + let ⟨K, κe⟩ := κ.Elaboration_total + let Eₛ : «F⊗⊕ω».Term := sorry + let .qual (.mono ρlc) := ρke.TypeVarLocallyClosed_of + let A₀lc := ρke.soundness Γcw Γwe κe.row |>.TypeVarLocallyClosed_of + let .qual (.mono ϕlc) := ϕke.TypeVarLocallyClosed_of + let A₁lc := ϕke.soundness Γcw Γwe (κe.arr .star) |>.TypeVarLocallyClosed_of + let .qual (.mono μlc) := μke.TypeVarLocallyClosed_of + let Mlc := Mte.TermVarLocallyClosed_of + let Ety := Mte.soundness (open KindingAndElaboration in by + show KindingAndElaboration _ _ _ _ [[∀ aₗ : *. ∀ aₜ : K. ∀ aₚ : L K. ∀ aᵢ : L K. ∀ aₙ : L K. (⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aₚ$3⟧)) → (⊗ (a$0 ⟦{aₜ$4}⟧)) → ⊗ (a$0 ⟦aᵢ$2⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦aₚ$4⟧)) → aₜ$0) → ((⊕ (a$1 ⟦{aₜ$5}⟧)) → aₜ$0) → (⊕ (a$1 ⟦aᵢ$3⟧)) → aₜ$0, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → ⊗ (a$0 ⟦aₚ$3⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aₚ$3⟧)) → ⊕ (a$0 ⟦aᵢ$2⟧)}, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → ⊗ (a$0 ⟦{aₜ$4}⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦{aₜ$4}⟧)) → ⊕ (a$0 ⟦aᵢ$2⟧)}}) → (⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → (⊗ (a$0 ⟦aₙ$1⟧)) → ⊗ (a$0 ⟦A₀⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦aᵢ$3⟧)) → aₜ$0) → ((⊕ (a$1 ⟦aₙ$2⟧)) → aₜ$0) → (⊕ (a$1 ⟦A₀⟧)) → aₜ$0, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀⟧)) → ⊗ (a$0 ⟦aᵢ$2⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aᵢ$2⟧)) → ⊕ (a$0 ⟦A₀⟧)}, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀⟧)) → ⊗ (a$0 ⟦aₙ$1⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aₙ$1⟧)) → ⊕ (a$0 ⟦A₀⟧)}}) → (⊗ { }) → A₁ aₜ$3]] + apply scheme Γ.typeVarDom _ .label + intro aₗ aₗnin + simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, + Type.TypeVar_open] + rw [ρlc.weakening (n := 4).TypeVar_open_id, ϕlc.weakening (n := 4).TypeVar_open_id, + A₀lc.weaken (n := 5).TypeVar_open_id, A₀lc.weaken (n := 6).TypeVar_open_id, + A₁lc.weaken (n := 4).TypeVar_open_id] + apply scheme (aₗ :: Γ.typeVarDom) _ κe + intro aₜ aₜnin + simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, + Type.TypeVar_open] + rw [ρlc.weakening (n := 3).TypeVar_open_id, ϕlc.weakening (n := 3).TypeVar_open_id, + A₀lc.weaken (n := 4).TypeVar_open_id, A₀lc.weaken (n := 5).TypeVar_open_id, + A₁lc.weaken (n := 3).TypeVar_open_id] + apply scheme (aₜ :: aₗ :: Γ.typeVarDom) _ κe.row + intro aₚ aₚnin + simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, + Type.TypeVar_open] + rw [ρlc.weakening (n := 2).TypeVar_open_id, ϕlc.weakening (n := 2).TypeVar_open_id, + A₀lc.weaken (n := 3).TypeVar_open_id, A₀lc.weaken (n := 4).TypeVar_open_id, + A₁lc.weaken (n := 2).TypeVar_open_id] + apply scheme (aₚ :: aₜ :: aₗ :: Γ.typeVarDom) _ κe.row + intro aᵢ aᵢnin + simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, + Type.TypeVar_open] + rw [ρlc.weakening (n := 1).TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, + A₀lc.weaken (n := 2).TypeVar_open_id, A₀lc.weaken (n := 3).TypeVar_open_id, + A₁lc.weaken (n := 1).TypeVar_open_id] + apply scheme (aᵢ :: aₚ :: aₜ :: aₗ :: Γ.typeVarDom) _ κe.row + intro aₙ aₙnin + simp [TypeScheme.TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, + Type.TypeVar_open] + rw [ρlc.TypeVar_open_id, ϕlc.TypeVar_open_id, A₀lc.weaken (n := 1).TypeVar_open_id, + A₀lc.weaken (n := 2).TypeVar_open_id, A₁lc.TypeVar_open_id] + apply qual + (.concat .comm (.var (.typeExt sorry (.typeExt sorry .head))) + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe + (.contain .comm (.var (.typeExt sorry (.typeExt sorry .head))) (.var (.typeExt sorry .head)) + κe) + (.contain .comm + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe)) _ .star + let Γawe := Γwe.typeExt aₗnin .label |>.typeExt aₜnin κe |>.typeExt aₚnin κe.row + |>.typeExt aᵢnin κe.row |>.typeExt aₙnin κe.row + let ρke' := ρke.weakening Γawe (Γ'' := .empty) + (Γ' := .typeExt (.typeExt (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) + apply qual + (.concat .comm (.var (.typeExt sorry .head)) (.var .head) ρke' κe + (.contain .comm (.var (.typeExt sorry .head)) ρke' κe) + (.contain .comm (.var .head) ρke' κe)) _ .star + exact .arr + (.floor (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head)))))) <| + ϕke.weakening Γawe (Γ'' := .empty) + (Γ' := .typeExt (.typeExt (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) |>.app <| + .var <| .typeExt sorry <| .typeExt sorry <| .typeExt sorry <| .head + ) Γᵢw Γcw Γwe + let Elc := Ety.TermVarLocallyClosed_of + let Etlc := Ety.TermTypeVarLocallyClosed_of + have : Monotype.prodOrSum .prod μ (.lift (.mk κ (.app ϕ (.var (.bound 0)))) ρ) = + .Monotype_open (.prodOrSum .prod μ (.lift (.mk κ (.app ϕ (.var (.bound 0)))) (.var (.bound 0)))) ρ := by + simp [Monotype.Monotype_open, TypeLambda.Monotype_open] + exact ⟨μlc.Monotype_open_id.symm, ϕlc.weakening (n := 1).Monotype_open_id.symm⟩ + rw [this] + apply Exists.intro [[⦅F [λ a : L K. ⊗ (λ a' : K. A₁ a'$0) ⟦a$0⟧] ⦅Λ aₗ : *. Λ aₜ : K. Λ aₚ : L K. Λ aᵢ : L K. Λ aₙ : L K. ⦅λ xₙₗ : ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aₚ$3⟧)) → (⊗ (a$0 ⟦{aₜ$4}⟧)) → ⊗ (a$0 ⟦aᵢ$2⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦aₚ$4⟧)) → aₜ$0) → ((⊕ (a$1 ⟦{aₜ$5}⟧)) → aₜ$0) → (⊕ (a$1 ⟦aᵢ$3⟧)) → aₜ$0, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → ⊗ (a$0 ⟦aₚ$3⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aₚ$3⟧)) → ⊕ (a$0 ⟦aᵢ$2⟧)}, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → ⊗ (a$0 ⟦{aₜ$4}⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦{aₜ$4}⟧)) → ⊕ (a$0 ⟦aᵢ$2⟧)}}. ⦅λ xₙᵣ : ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦aᵢ$2⟧)) → (⊗ (a$0 ⟦aₙ$1⟧)) → ⊗ (a$0 ⟦A₀⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦aᵢ$3⟧)) → aₜ$0) → ((⊕ (a$1 ⟦aₙ$2⟧)) → aₜ$0) → (⊕ (a$1 ⟦A₀⟧)) → aₜ$0, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀⟧)) → ⊗ (a$0 ⟦aᵢ$2⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aᵢ$2⟧)) → ⊕ (a$0 ⟦A₀⟧)}, ⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀⟧)) → ⊗ (a$0 ⟦aₙ$1⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦aₙ$1⟧)) → ⊕ (a$0 ⟦A₀⟧)}}. ⦅λ xₗ : ⊗ { }. ⦅λ xₐ : ⊗ ((λ a' : K. A₁ a'$0) ⟦aₚ$2⟧). ⦅E ⦅λ xₙₗ' : A₀. ⦅⦅π 0 xₙₗ'$0⦆ [λ a' : *. a'$0] xₐ$1⦆ ⦅⦅λ x : ⊗ {A₁}. x$0⦆ (⦅⦅E [aₗ$4] [aₜ$3] [aₚ$2] [aᵢ$1] [aₙ$0] xₙₗ$4⦆ xₙᵣ$3⦆ xₗ$2)⦆⦆⦆ xₙₗ$3⦆⦆⦆⦆⦆⦆ ⦅⦅⦅Λ a : * ↦ *. λ x : ⊗ (a$0 ⟦(λ a' : K. A₁ a'$0) ⟦{ }⟧⟧). x$0⦆ [λ a : *. a$0]⦆ ⦅⦅λ x : ⊗ { }. x$0⦆ ()⦆⦆]] + apply «ind» Γ.typeVarDom Γ.typeVarDom ρke _ κe _ _ indce + · intro a anin + let Γawe := Γwe.typeExt anin κe.row + simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open, Type.TypeVar_open] + rw [μlc.TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, + A₁lc.weaken (n := 1).TypeVar_open_id] + apply KindingAndElaboration.prod <| μke.weakening Γawe (Γ' := .typeExt .empty ..) (Γ'' := .empty) + apply KindingAndElaboration.lift (a :: Γ.typeVarDom) _ κe <| .var .head + intro a' a'nin + let Γaa'we := Γawe.typeExt a'nin κe + simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open, Type.TypeVar_open] + rw [ϕlc.TypeVar_open_id, A₁lc.TypeVar_open_id] + exact .app (ϕke.weakening Γaa'we (Γ' := .typeExt (.typeExt .empty ..) ..) (Γ'' := .empty)) <| + .var .head + · intro aₗ aₗnin aₜ aₜnin aₚ aₚnin aᵢ aᵢnin aₙ aₙnin + let Γawe := Γwe.typeExt aₗnin .label |>.typeExt aₜnin κe |>.typeExt aₚnin κe.row + |>.typeExt aᵢnin κe.row |>.typeExt aₙnin κe.row + simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open, «F⊗⊕ω».Term.TypeVar_open, + Type.TypeVar_open] + rw [μlc.TypeVar_open_id, μlc.TypeVar_open_id, ϕlc.weakening (n := 1).TypeVar_open_id, + ϕlc.weakening (n := 1).TypeVar_open_id, Etlc.weaken (n := 4).TypeVar_open_id, + Etlc.weaken (n := 3).TypeVar_open_id, Etlc.weaken (n := 2).TypeVar_open_id, + Etlc.weaken (n := 1).TypeVar_open_id, Etlc.TypeVar_open_id, + A₀lc.weaken (n := 5).TypeVar_open_id, A₀lc.weaken (n := 6).TypeVar_open_id, + A₀lc.weaken (n := 4).TypeVar_open_id, A₀lc.weaken (n := 5).TypeVar_open_id, + A₀lc.weaken (n := 3).TypeVar_open_id, A₀lc.weaken (n := 4).TypeVar_open_id, + A₀lc.weaken (n := 2).TypeVar_open_id, A₀lc.weaken (n := 3).TypeVar_open_id, + A₀lc.weaken (n := 1).TypeVar_open_id, A₀lc.weaken (n := 2).TypeVar_open_id, + A₁lc.weaken (n := 5).TypeVar_open_id, A₁lc.weaken (n := 4).TypeVar_open_id, + A₁lc.weaken (n := 3).TypeVar_open_id, A₁lc.weaken (n := 4).TypeVar_open_id, + A₁lc.weaken (n := 2).TypeVar_open_id, A₁lc.weaken (n := 3).TypeVar_open_id, + A₁lc.weaken (n := 1).TypeVar_open_id, A₁lc.weaken (n := 2).TypeVar_open_id, + A₁lc.weaken (n := 1).TypeVar_open_id] + apply qualI Γ.termVarDom <| + .concat .comm (.var (.typeExt sorry (.typeExt sorry .head))) + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe + (.contain .comm (.var (.typeExt sorry (.typeExt sorry .head))) (.var (.typeExt sorry .head)) + κe) + (.contain .comm + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe) + intro xₙₗ xₙₗnin + let Γaxₙₗwe := Γawe.constrExt xₙₗnin <| + .concat (.comm (u := .non)) (.var (.typeExt sorry (.typeExt sorry .head))) + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe + (.contain .comm (.var (.typeExt sorry (.typeExt sorry .head))) (.var (.typeExt sorry .head)) + κe) + (.contain .comm + (.singleton_row + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry (.typeExt sorry (.typeExt sorry .head))))) + (.var (.typeExt sorry .head)) κe) + let ρke' := ρke.weakening Γaxₙₗwe (Γ'' := .empty) (Γ' := .constrExt (.typeExt (.typeExt + (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) + simp [«F⊗⊕ω».Term.TermVar_open] + rw [Elc.weaken (n := 4).TermVar_open_id] + apply qualI (xₙₗ :: Γ.termVarDom) <| + .concat .comm (.var (.constrExt (.typeExt sorry .head))) (.var (.constrExt .head)) + ρke' κe (.contain .comm (.var (.constrExt (.typeExt sorry .head))) ρke' κe) + (.contain .comm (.var (.constrExt .head)) ρke' κe) + intro xₙᵣ xₙᵣnin + let Γaxₙₗᵣwe := Γaxₙₗwe.constrExt xₙᵣnin <| + .concat (.comm (u := .non)) (.var (.constrExt (.typeExt sorry .head))) + (.var (.constrExt .head)) ρke' κe + (.contain .comm (.var (.constrExt (.typeExt sorry .head))) ρke' κe) + (.contain .comm (.var (.constrExt .head)) ρke' κe) + simp [«F⊗⊕ω».Term.TermVar_open] + rw [Elc.weaken (n := 3).TermVar_open_id] + apply lam (xₙᵣ :: xₙₗ :: Γ.termVarDom) _ <| .floor <| .var <| .constrExt <| .constrExt <| + .typeExt sorry <| .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head + intro xₗ xₗnin + let Γaxₙₗᵣxₗwe := Γaxₙₗᵣwe.termExt xₗnin <| .floor <| .var <| .constrExt <| .constrExt <| + .typeExt sorry <| .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head + simp [Term.TermVar_open, «F⊗⊕ω».Term.TermVar_open] + rw [Mlc.weakening (n := 1).TermVar_open_id, Elc.weaken (n := 2).TermVar_open_id] + let μke' := μke.weakening Γaxₙₗᵣxₗwe (Γ'' := .empty) (Γ' := .termExt (.constrExt (.constrExt + (.typeExt (.typeExt (.typeExt (.typeExt (.typeExt .empty ..) ..) ..) ..) ..) ..) ..) ..) + apply lam (xₗ :: xₙᵣ :: xₙₗ :: Γ.termVarDom) _ <| .prod μke' <| + .lift (aₙ :: aᵢ :: aₚ :: aₜ :: aₗ :: Γ.typeVarDom) (by + intro a' a'nin + let Γaxₙₗᵣxₗa'we := Γaxₙₗᵣxₗwe.typeExt a'nin κe + simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open, «F⊗⊕ω».Term.TypeVar_open, + Type.TypeVar_open] + rw [ϕlc.TypeVar_open_id, A₁lc.TypeVar_open_id] + exact ϕke.weakening Γaxₙₗᵣxₗa'we (Γ'' := .empty) (Γ' := .typeExt (.termExt (.constrExt + (.constrExt (.typeExt (.typeExt (.typeExt (.typeExt (.typeExt + .empty ..) ..) ..) ..) ..) ..) ..) ..) ..) |>.app <| .var .head + ) κe <| .var <| .termExt <| .constrExt <| .constrExt <| .typeExt sorry <| .typeExt sorry .head + intro xₐ xₐnin + let Γaxₙₗᵣxₗₐwe := Γaxₙₗᵣxₗwe.termExt xₐnin <| .prod μke' <| + .lift (aₙ :: aᵢ :: aₚ :: aₜ :: aₗ :: Γ.typeVarDom) (by + intro a' a'nin + show KindingAndElaboration _ _ (.qual (.mono (.TypeVar_open (ϕ.app (.var (.bound 0))) a'))) + _ (.TypeVar_open (A₁.app (.var (.bound 0))) a') + let Γaxₙₗᵣxₗa'we := Γaxₙₗᵣxₗwe.typeExt a'nin κe + simp [Monotype.TypeVar_open, TypeLambda.TypeVar_open, «F⊗⊕ω».Term.TypeVar_open, + Type.TypeVar_open] + rw [ϕlc.TypeVar_open_id, A₁lc.TypeVar_open_id] + exact ϕke.weakening Γaxₙₗᵣxₗa'we (Γ'' := .empty) (Γ' := .typeExt (.termExt (.constrExt + (.constrExt (.typeExt (.typeExt (.typeExt (.typeExt (.typeExt + .empty ..) ..) ..) ..) ..) ..) ..) ..) ..) |>.app <| .var .head + ) κe <| .var <| .termExt <| .constrExt <| .constrExt <| .typeExt sorry <| .typeExt sorry .head + simp [Term.TermVar_open, «F⊗⊕ω».Term.TermVar_open] + rw [Mlc.TermVar_open_id, Elc.weaken (n := 1).TermVar_open_id] + apply qualE <| .local <| .termExt sorry <| .termExt sorry <| .constrExt sorry .head + apply sub _ (by + show _ + ) (σ₀ := .qual + (.qual + (.concat + (lift (.mk κ (ϕ.app (.var (.bound 0)))) (.var (.free aₚ))) μ + (row [(.var (.free aₗ), ϕ.app (.var (.free aₜ)))] none) + (lift (.mk κ (ϕ.app (.var (.bound 0)))) (.var (.free aᵢ)))) + (.mono (prodOrSum .prod μ (lift (.mk κ (ϕ.app (.var (.bound 0)))) (.var (.free aᵢ))))))) + apply qualI (xₐ :: xₗ :: xₙᵣ :: xₙₗ :: Γ.termVarDom) sorry + intro xₙₗ' xₙₗ'nin + simp [«F⊗⊕ω».Term.TermVar_open] + apply TypingAndElaboration.concat (.var (.constrExt sorry .head)) _ <| .local .head + apply singleton_prod (.var (.constrExt sorry (.termExt sorry .head))) ?h (.var (.constrExt (.termExt (.termExt (.constrExt (.constrExt (.typeExt sorry (.typeExt sorry (.typeExt sorry (.typeExt sorry .head)))))))))) + case h => + apply TypingAndElaboration.app _ <| .var <| .constrExt sorry <| .termExt sorry .head + let Mte' := Mte.weakening Γaxₙₗᵣxₗₐwe (Γ'' := .empty) (Γ' := .termExt (.termExt (.constrExt + (.constrExt (.typeExt (.typeExt (.typeExt (.typeExt (.typeExt + .empty ..) ..) ..) ..) ..) ..) ..) ..) ..) + let Mte'' := Mte'.schemeE <| .var <| .termExt <| .termExt <| .constrExt <| .constrExt <| + .typeExt sorry <| .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head + simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, + Monotype.Monotype_open] at Mte'' + let Mte''' := Mte''.schemeE <| .var <| .termExt <| .termExt <| .constrExt <| .constrExt <| + .typeExt sorry <| .typeExt sorry <| .typeExt sorry .head + simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, + Monotype.Monotype_open] at Mte''' + let Mte'''' := Mte'''.schemeE <| .var <| .termExt <| .termExt <| .constrExt <| .constrExt <| + .typeExt sorry <| .typeExt sorry .head + simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, + Monotype.Monotype_open] at Mte'''' + let Mte''''' := Mte''''.schemeE <| .var <| .termExt <| .termExt <| .constrExt <| + .constrExt <| .typeExt sorry .head + simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, + Monotype.Monotype_open] at Mte''''' + let Mte'''''' := Mte'''''.schemeE <| .var <| .termExt <| .termExt <| .constrExt <| + .constrExt .head + simp [TypeScheme.Monotype_open, QualifiedType.Monotype_open, + Monotype.Monotype_open] at Mte'''''' + rw [ρlc.weakening (n := 4).Monotype_open_id, ρlc.weakening (n := 3).Monotype_open_id, + ρlc.weakening (n := 2).Monotype_open_id, ρlc.weakening (n := 1).Monotype_open_id, + ρlc.Monotype_open_id, ϕlc.weakening (n := 4).Monotype_open_id, + ϕlc.weakening (n := 3).Monotype_open_id, ϕlc.weakening (n := 2).Monotype_open_id, + ϕlc.weakening (n := 1).Monotype_open_id, ϕlc.Monotype_open_id] at Mte'''''' + apply qualE (.local (.termExt sorry (.termExt sorry (.constrExt sorry .head)))) at Mte'''''' + apply qualE (.local (.termExt sorry (.termExt sorry .head))) at Mte'''''' + exact Mte'''''' + · simp [Monotype.Monotype_open, TypeLambda.Monotype_open] + rw [μlc.Monotype_open_id, ϕlc.weakening (n := 1).Monotype_open_id] + apply sub <| .unit μke + apply SubtypingAndElaboration.prodRow _ <| .prod μke .empty_row + swap + let liftee := RowEquivalenceAndElaboration.liftR μ (.lift Γ.typeVarDom (by + intro a' a'nin + let Γa'we := Γwe.typeExt a'nin κe + show KindingAndElaboration _ _ (.qual (.mono (.TypeVar_open (ϕ.app (.var (.bound 0))) a'))) _ (.TypeVar_open (A₁.app (.var (.bound 0))) a') + simp [Monotype.TypeVar_open, Type.TypeVar_open] + rw [ϕlc.TypeVar_open_id, A₁lc.TypeVar_open_id] + exact ϕke.weakening Γa'we (Γ' := .typeExt .empty ..) (Γ'' := .empty) |>.app <| .var .head + ) κe (by + rw [Range.map_same_eq_nil, Option.someIf, if_pos rfl] + exact .empty_row + · exact fun _ => default + · exact fun _ => default)) .star (n := 0) (Γc := Γc) (Γ := Γ) + rw [Range.map_same_eq_nil, Range.map_same_eq_nil, Option.someIf, if_pos rfl, Option.someIf, + if_pos rfl] at liftee + exact liftee + +-- theorem fold_emulation (ρke : [[Γc; Γ ⊢ ρ : R κ ⇝ A₀]]) (μke : [[Γc; Γ ⊢ μ : U ⇝ B]]) +-- (τke : [[Γc; Γ ⊢ τ : * ⇝ A₁]]) +-- (M₁te : [[Γᵢ; Γc; Γ ⊢ M₁ : ∀ aₗ : L. ∀ aₜ : *. ∀ aₚ : R *. ∀ aᵢ : R *. ∀ aₙ : R *. aₚ$2 ⊙(N) ⟨aₗ$4 ▹ aₜ$3⟩ ~ aᵢ$1 ⇒ aᵢ$1 ⊙(N) aₙ$0 ~ ρ ⇒ ⌊aₗ$4⌋ → aₜ$3 → τ ⇝ E₁]]) +-- (M₂te : [[Γᵢ; Γc; Γ ⊢ M₂ : τ → τ → τ ⇝ E₂]]) (M₃te : [[Γᵢ; Γc; Γ ⊢ M₃ : τ ⇝ E₂]]) +-- (Nty : [[Γᵢ; Γc; Γ ⊢ «N» : Π(μ) ρ ⇝ E₂]]) (indce : [[Γᵢ; Γc; Γ ⊨ Ind ρ ⇝ F]]) (Γᵢw : [[Γc ⊢ Γᵢ]]) +-- (Γcw : [[⊢c Γc]]) (Γwe : [[Γc ⊢ Γ ⇝ Δ]]) +-- : ∃ F, [[Γᵢ; Γc; Γ ⊢ ind (λ a : R κ. τ) ρ; (λ xₗ. λ xₐ. (M₂ xₐ$0) ((M₁ xₗ$1) ((prj «N»)/xₗ$1))); M₃ : τ ⇝ F]] := sorry + +end TabularTypeInterpreter diff --git a/tex/TabularTypeInterpreter/Term/TypingAndElaboration.tex b/tex/TabularTypeInterpreter/Term/TypingAndElaboration.tex index e05cfe5..bd97406 100644 --- a/tex/TabularTypeInterpreter/Term/TypingAndElaboration.tex +++ b/tex/TabularTypeInterpreter/Term/TypingAndElaboration.tex @@ -1 +1 @@ -\lottjudgement{Typing And Elaboration}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}{\lottinferencerule{var}{\lotthypothesis{\sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{∈} \, \sourcepre Γ \sourcepost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre x \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre x \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{lam}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{λ} \, \sourcepre x \sourcepost \lottsym{.} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{app}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{qualI}{\lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{C} \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre ψ \sourcepost \, \lottsym{⇝} \, \targetpre x \targetpost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre γ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \, \lottsym{⇒} \, \sourcepre γ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{qualE}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre ψ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \, \lottsym{⇒} \, \sourcepre γ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre γ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{schemeI}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost} \\ \lotthypothesis{\lottsym{⊢} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre K \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \lottsym{∀} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{.} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{Λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{schemeE}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \lottsym{∀} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{.} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost\left[\sourcepre τ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost} \lottinferencerulesep \lottinferencerule{let}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre σ₀ \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{let} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \, \lottsym{=} \, \sourcepre M \sourcepost \, \lottkw{in} \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{annot}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{label}{\\\\}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre ℓ \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre \sourcepre ℓ \sourcepost \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{(} \lottsym{)} \targetpost} \lottinferencerulesep \lottinferencerule{prod}{\lotthypothesis{\lottjudgementcomprehension{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre {M}_{i} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre {ξ}_{i} \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre {F}_{i} \targetpost}} \\ \lotthypothesis{\lottkw{unique} \lottsym{(} \lottsepbycomprehension{\sourcepre {ξ}_{i} \sourcepost} \lottsym{)}} \\ \lotthypothesis{\lottjudgementcomprehension{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre {N}_{i} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {τ}_{i} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre {E}_{i} \targetpost}}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{\{} \lottsepbycomprehension{\sourcepre {M}_{i} \sourcepost \, \lottsym{▹} \, \sourcepre {N}_{i} \sourcepost} \lottsym{\}} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \lottsepbycomprehension{\sourcepre {ξ}_{i} \sourcepost \, \lottsym{▹} \, \sourcepre {τ}_{i} \sourcepost} \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{(} \lottsepbycomprehension{\targetpre {E}_{i} \targetpost} \lottsym{)} \targetpost} \lottinferencerulesep \lottinferencerule{sum}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{[} \sourcepre M \sourcepost \, \lottsym{▹} \, \sourcepre N \sourcepost \lottsym{]} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{ι}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{unlabelProd}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \lottsym{/} \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{π}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{unlabelSum}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \lottsym{/} \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottkw{case} \, \targetpre E \targetpost \, \lottsym{\{} \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre \targetpre x \targetpost \targetpost \targetpost \lottsym{\}} \targetpost} \lottinferencerulesep \lottinferencerule{prj}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₁ \sourcepost \, \lottsym{≲}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{prj} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{concat}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{⊙}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \, \lottsym{\sim} \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \doubleplus \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{inj}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{≲}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{inj} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{elim}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{⊙}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \, \lottsym{\sim} \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \lottsym{▿} \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{sub}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{<:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{member}{\lotthypothesis{\sourcepre \lottsym{(} \lottsepbycomprehension{\sourcepre {TCₛ}_{i} \sourcepost \, \sourcepre a \sourcepost \, \lottsym{⇝} \, \targetpre {Aₛ}_{i} \targetpost} \, \lottsym{⇒} \, \sourcepre TC \sourcepost \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{)} \, \lottsym{↦} \, \sourcepre m \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost \sourcepost \, \lottsym{∈} \, \sourcepre Γ_{C} \sourcepost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre TC \sourcepost \, \sourcepre τ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre m \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost\left[\sourcepre τ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{π}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{order}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre Ξ \sourcepost}_{\sourcepre \sourcepre \lottkw{C} \sourcepost \sourcepost} \, \sourcepre ρ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{order} \, \sourcepre ρ \sourcepost \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre Ξ \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre ρ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{ind}{\lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre ρ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre B \targetpost \targetpost} \\ \lotthypothesis{\lottsym{⊢} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre K \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre aₗ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{L} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₜ \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₚ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aᵢ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₙ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre aₚ \sourcepost \sourcepost \, \lottsym{⊙}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre \sourcepre aₗ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre \sourcepre aₜ \sourcepost \sourcepost \lottsym{⟩} \sourcepost \, \lottsym{\sim} \, \sourcepre \sourcepre aᵢ \sourcepost \sourcepost \sourcepost \, \lottsym{⇒} \, \sourcepre \sourcepre \sourcepre \sourcepre aᵢ \sourcepost \sourcepost \, \lottsym{⊙}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \sourcepre aₙ \sourcepost \sourcepost \, \lottsym{\sim} \, \sourcepre ρ \sourcepost \sourcepost \, \lottsym{⇒} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre \sourcepre aₗ \sourcepost \sourcepost \lottsym{⌋} \sourcepost \, \lottsym{→} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \, \lottsym{→} \, \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \targetpre \targetpre \targetpre E₀ \targetpost \targetpost \targetpost \targetpost \targetpost \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost\left[\sourcepre \lottsym{⟨} \lottsym{⟩} \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Ind} \, \sourcepre ρ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lottlet{\targetpre E \targetpost}{\targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre F \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre B \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre \lottsym{(} \targetpre \lottsym{Λ} \, \targetpre aₗ \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₜ \targetpost \, \lottsym{:} \, \targetpre K \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₚ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aᵢ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₙ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre E₀ \targetpost \targetpost \targetpost \targetpost \targetpost \targetpost \lottsym{)} \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{ind} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \sourcepre ρ \sourcepost \, \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost\left[\sourcepre ρ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{splitP}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Split} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \, \sourcepre ρ₁ \sourcepost \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lottlet{\targetpre E \targetpost}{\targetpre \lottsym{(} \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre \lottsym{π}_{2} \, \targetpre F \targetpost \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{,} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre \lottsym{π}_{3} \, \targetpre F \targetpost \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{splitₚ} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre \sourcepre ℓₘ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottkw{Lift} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \lottsym{,} \, \sourcepre \sourcepre ℓᵣ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{splitS}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{(} \sourcepre \lottkw{Lift} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ₀ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \sourcepost \lottsym{)} \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Split} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ₀ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \, \sourcepre ρ₁ \sourcepost \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{splitₛ} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost}} +\lottjudgement{Typing And Elaboration}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}{\lottinferencerule{var}{\lotthypothesis{\sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{∈} \, \sourcepre Γ \sourcepost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre x \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre x \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{lam}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{λ} \, \sourcepre x \sourcepost \lottsym{.} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{app}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₀ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{qualI}{\lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{C} \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre ψ \sourcepost \, \lottsym{⇝} \, \targetpre x \targetpost \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre γ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \, \lottsym{⇒} \, \sourcepre γ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{qualE}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre ψ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre ψ \sourcepost \, \lottsym{⇒} \, \sourcepre γ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre γ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{schemeI}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \targetpost} \\ \lotthypothesis{\lottsym{⊢} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre K \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \lottsym{∀} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{.} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{Λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K \targetpost \lottsym{.} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{schemeE}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \lottsym{∀} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{.} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost\left[\sourcepre τ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre E \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost} \lottinferencerulesep \lottinferencerule{let}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre σ₀ \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{let} \, \sourcepre x \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \, \lottsym{=} \, \sourcepre M \sourcepost \, \lottkw{in} \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{annot}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{label}{\\\\}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre ℓ \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre \sourcepre ℓ \sourcepost \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{(} \lottsym{)} \targetpost} \lottinferencerulesep \lottinferencerule{prod}{\lotthypothesis{\lottjudgementcomprehension{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre {M}_{i} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre {ξ}_{i} \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre {F}_{i} \targetpost}} \\ \lotthypothesis{\lottkw{unique} \lottsym{(} \lottsepbycomprehension{\sourcepre {ξ}_{i} \sourcepost} \lottsym{)}} \\ \lotthypothesis{\lottjudgementcomprehension{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre {N}_{i} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {τ}_{i} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre {E}_{i} \targetpost}}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{\{} \lottsepbycomprehension{\sourcepre {M}_{i} \sourcepost \, \lottsym{▹} \, \sourcepre {N}_{i} \sourcepost} \lottsym{\}} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \lottsepbycomprehension{\sourcepre {ξ}_{i} \sourcepost \, \lottsym{▹} \, \sourcepre {τ}_{i} \sourcepost} \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{(} \lottsepbycomprehension{\targetpre {E}_{i} \targetpost} \lottsym{)} \targetpost} \lottinferencerulesep \lottinferencerule{sum}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottsym{[} \sourcepre M \sourcepost \, \lottsym{▹} \, \sourcepre N \sourcepost \lottsym{]} \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{ι}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{unlabelProd}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \lottsym{/} \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{π}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{unlabelSum}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre ξ \sourcepost \, \lottsym{▹} \, \sourcepre τ \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre ξ \sourcepost \lottsym{⌋} \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \lottsym{/} \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \lottkw{case} \, \targetpre E \targetpost \, \lottsym{\{} \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre A \targetpost \lottsym{.} \, \targetpre \targetpre x \targetpost \targetpost \targetpost \lottsym{\}} \targetpost} \lottinferencerulesep \lottinferencerule{prj}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₁ \sourcepost \, \lottsym{≲}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{prj} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{concat}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{⊙}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \, \lottsym{\sim} \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \doubleplus \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{inj}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{≲}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{inj} \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{elim}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₀ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre ρ₀ \sourcepost \, \lottsym{⊙}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \, \lottsym{\sim} \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre M \sourcepost \, \lottsym{▿} \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{sub}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ₀ \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre σ₀ \sourcepost \, \lottsym{<:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre σ₁ \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre F \targetpost \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{member}{\lotthypothesis{\sourcepre \lottsym{(} \lottsepbycomprehension{\sourcepre {TCₛ}_{i} \sourcepost \, \sourcepre a \sourcepost \, \lottsym{⇝} \, \targetpre {Aₛ}_{i} \targetpost} \, \lottsym{⇒} \, \sourcepre TC \sourcepost \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \lottsym{)} \, \lottsym{↦} \, \sourcepre m \sourcepost \, \lottsym{:} \, \sourcepre σ \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost \sourcepost \, \lottsym{∈} \, \sourcepre Γ_{C} \sourcepost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \sourcepre TC \sourcepost \, \sourcepre τ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre m \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre σ \sourcepost\left[\sourcepre τ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \, \lottsym{⇝} \, \targetpre \lottsym{π}_{0} \, \targetpre E \targetpost \targetpost} \lottinferencerulesep \lottinferencerule{order}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre Ξ \sourcepost}_{\sourcepre \sourcepre \lottkw{C} \sourcepost \sourcepost} \, \sourcepre ρ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{order} \, \sourcepre ρ \sourcepost \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre Ξ \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre ρ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{ind}{\lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre ρ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre B \targetpost \targetpost} \\ \lotthypothesis{\lottsym{⊢} \, \sourcepre κ \sourcepost \, \lottsym{⇝} \, \targetpre K \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre Γ \sourcepost \lottsym{,} \, \sourcepre aₗ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{L} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₜ \sourcepost \, \lottsym{:} \, \sourcepre κ \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₚ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aᵢ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \lottsym{,} \, \sourcepre aₙ \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \sourcepre aₚ \sourcepost \sourcepost \, \lottsym{⊙}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre \sourcepre aₗ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre \sourcepre aₜ \sourcepost \sourcepost \lottsym{⟩} \sourcepost \, \lottsym{\sim} \, \sourcepre \sourcepre aᵢ \sourcepost \sourcepost \sourcepost \, \lottsym{⇒} \, \sourcepre \sourcepre \sourcepre \sourcepre aᵢ \sourcepost \sourcepost \, \lottsym{⊙}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \sourcepre aₙ \sourcepost \sourcepost \, \lottsym{\sim} \, \sourcepre ρ \sourcepost \sourcepost \, \lottsym{⇒} \, \sourcepre \sourcepre \sourcepre \lottsym{⌊} \sourcepre \sourcepre aₗ \sourcepost \sourcepost \lottsym{⌋} \sourcepost \, \lottsym{→} \, \sourcepre \sourcepre \sourcepre τ \sourcepost \sourcepost \, \lottsym{→} \, \sourcepre \sourcepre τ \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \targetpre \targetpre \targetpre \targetpre E₀ \targetpost \targetpost \targetpost \targetpost \targetpost \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost\left[\sourcepre \lottsym{⟨} \lottsym{⟩} \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Ind} \, \sourcepre ρ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lottlet{\targetpre E \targetpost}{\targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre F \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre B \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre \lottsym{(} \targetpre \lottsym{Λ} \, \targetpre aₗ \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₜ \targetpost \, \lottsym{:} \, \targetpre K \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₚ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aᵢ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre \lottsym{Λ} \, \targetpre aₙ \targetpost \, \lottsym{:} \, \targetpre \lottkw{L}^{\targetpre K \targetpost} \targetpost \lottsym{.} \, \targetpre E₀ \targetpost \targetpost \targetpost \targetpost \targetpost \targetpost \lottsym{)} \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{ind} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \lottkw{R}^{\sourcepre κ \sourcepost} \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \sourcepre ρ \sourcepost \, \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre τ \sourcepost\left[\sourcepre ρ \sourcepost/\sourcepre a \sourcepost\right] \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{splitP}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Split} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \, \sourcepre ρ₁ \sourcepost \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lottlet{\targetpre E \targetpost}{\targetpre \lottsym{(} \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre \lottsym{π}_{2} \, \targetpre F \targetpost \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{,} \, \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{0} \, \targetpre \lottsym{π}_{3} \, \targetpre F \targetpost \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{splitₚ} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre M \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre \sourcepre \lottkw{N} \sourcepost \sourcepost} \, \sourcepre \lottsym{⟨} \sourcepre \sourcepre ℓₘ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottkw{Lift} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \sourcepost \sourcepost \lottsym{,} \, \sourcepre \sourcepre ℓᵣ \sourcepost \sourcepost \, \lottsym{▹} \, \sourcepre {\sourcepre \lottsym{Π} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{⟩} \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E \targetpost} \lottinferencerulesep \lottinferencerule{splitS}{\lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre M \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre \lottsym{(} \sourcepre \lottkw{Lift} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ₀ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \sourcepost \lottsym{)} \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₀ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre N \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₁ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre E₁ \targetpost} \\ \lotthypothesis{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊨} \, \sourcepre \lottkw{Split} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ₀ \sourcepost \lottsym{)} \sourcepost \, \sourcepre ρ₀ \sourcepost \, \sourcepre ρ₁ \sourcepost \, \sourcepre ρ₂ \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre F \targetpost} \\ \lotthypothesis{\sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \sourcepre \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \, \lottsym{⇝} \, \targetpre A \targetpost}}{\sourcepre Γ_{I} \sourcepost \lottsym{;} \, \sourcepre Γ_{C} \sourcepost \lottsym{;} \, \sourcepre Γ \sourcepost \, \lottsym{⊢} \, \sourcepre \lottkw{splitₛ} \, \sourcepre \lottsym{(} \lottsym{λ} \, \sourcepre a \sourcepost \, \lottsym{:} \, \sourcepre \star \sourcepost \lottsym{.} \, \sourcepre τ \sourcepost \lottsym{)} \sourcepost \sourcepre M \sourcepost \, \sourcepre N \sourcepost \sourcepost \, \lottsym{:} \, \sourcepre \sourcepre \sourcepre \sourcepre \lottsym{(} \sourcepre {\sourcepre \lottsym{Σ} \sourcepost}_{\sourcepre μ \sourcepost} \, \sourcepre ρ₂ \sourcepost \sourcepost \lottsym{)} \sourcepost \, \lottsym{→} \, \sourcepre τ₁ \sourcepost \sourcepost \sourcepost \sourcepost \, \lottsym{⇝} \, \targetpre \targetpre \lottsym{(} \targetpre \targetpre \targetpre \targetpre \lottsym{(} \targetpre \lottsym{π}_{1} \, \targetpre F \targetpost \targetpost \lottsym{)} \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \star \targetpost \lottsym{.} \, \targetpre \targetpre a \targetpost \targetpost \targetpost \lottsym{]} \targetpost \, \lottsym{[} \targetpre A \targetpost \lottsym{]} \targetpost \, \targetpre E₀ \targetpost \targetpost \lottsym{)} \targetpost \, \targetpre E₁ \targetpost \targetpost}}