import TabularTypes.«F⊗⊕ω».Lemmas.Type import TabularTypes.Lemmas.TypeEnvironment.Basic import TabularTypes.Theorems.Kind import TabularTypes.Theorems.Type.KindingAndElaboration namespace TabularTypes open Std namespace «F⊗⊕ω».Type private theorem contain_evidence_eq_inversion (aninA : a ∉ A.freeTypeVars) (eq : A.TypeVar_open a n = [[⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₁⟧)) → ⊗ (a$0 ⟦A₀⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦A₀⟧)) → ⊕ (a$0 ⟦A₁⟧)}]]) : ∃ A₀' A₁', A₀ = A₀'.TypeVar_open a (n + 1) ∧ A₁ = A₁'.TypeVar_open a (n + 1) ∧ A = [[⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₁'⟧)) → ⊗ (a$0 ⟦A₀'⟧), ∀ a : K ↦ *. (⊕ (a$0 ⟦A₀'⟧)) → ⊕ (a$0 ⟦A₁'⟧)}]] := by cases A <;> rw [TypeVar_open] at * case prod => rename «Type» => A let eq' := prod.inj eq cases A <;> rw [TypeVar_open] at * case list => rcases list.inj eq' with ⟨eq'', rfl⟩ rw [List.mapMem_eq_map] at * rename List _ => As match As with | [] => nomatch eq'' | A₀' :: As' => rw [List.map_cons] at * match As' with | [] => generalize A₀'.TypeVar_open a n = A₀'' at * nomatch eq'' | A₁' :: As'' => rw [List.map_cons] at * match As'' with | A₂' :: _ => generalize A₀'.TypeVar_open a n = A₀'' at * generalize A₁'.TypeVar_open a n = A₁'' at * generalize A₂'.TypeVar_open a n = A₂'' at * nomatch eq'' | [] => rw [List.map_nil] at * let ⟨eq₀, eq'''⟩ := List.cons_eq_cons.mp eq'' let eq₁ := List.singleton_inj.mp eq''' cases A₀' <;> rw [TypeVar_open] at * case «forall» => let ⟨Keq, eq₀'⟩ := forall.inj eq₀ cases Keq rename «Type» => A₀' cases A₀' <;> rw [Type.TypeVar_open] at * case arr => rename_i A₀₀' A₀₁' cases A₀₀' <;> rw [Type.TypeVar_open] at * case prod => rename «Type» => A₀₀' cases A₀₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₀₀₀' A₀₀₁' cases A₀₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₀₁' <;> rw [Type.TypeVar_open] at * case prod => rename «Type» => A₀₀' cases A₀₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₀₁₀' A₀₁₁' cases A₀₁₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₁' <;> rw [TypeVar_open] at * case «forall» => let ⟨Keq, eq₁'⟩ := forall.inj eq₁ cases Keq rename «Type» => A₁' cases A₁' <;> rw [Type.TypeVar_open] at * case arr => rename_i A₁₀' A₁₁' cases A₁₀' <;> rw [Type.TypeVar_open] at * case sum => rename «Type» => A₁₀' cases A₁₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₁₀₀' A₁₀₁' cases A₁₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₁₁' <;> rw [Type.TypeVar_open] at * case sum => rename «Type» => A₁₀' cases A₁₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₁₁₀' A₁₁₁' cases A₁₁₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases eq₀' let ⟨eq₁₀, eq₁₁⟩ := arr.inj eq₁' simp [freeTypeVars] at aninA let ⟨ aninA₀₀₁', aninA₀₁₁', aninA₁₀₁', aninA₁₁₁' ⟩ := aninA cases TypeVar_open_inj_of_not_mem_freeTypeVars aninA₁₀₁' aninA₀₁₁' <| And.right <| listApp.inj <| sum.inj eq₁₀ cases TypeVar_open_inj_of_not_mem_freeTypeVars aninA₁₁₁' aninA₀₀₁' <| And.right <| listApp.inj <| sum.inj eq₁₁ exact ⟨_, _, rfl, rfl, rfl⟩ | _ + 1 => split at eq₁' <;> nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' | _ + 1 => split at eq₁' <;> nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁' all_goals nomatch eq₁ | _ + 1 => split at eq₀' <;> nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' | _ + 1 => split at eq₀' <;> nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀ all_goals nomatch eq all_goals nomatch eq set_option maxHeartbeats 2000000 in private theorem concat_evidence_eq_inversion (eq : A.TypeVar_open a n = [[⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀⟧)) → (⊗ (a$0 ⟦A₁⟧)) → ⊗ (a$0 ⟦A₂⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦A₀⟧)) → aₜ$0) → ((⊕ (a$1 ⟦A₁⟧)) → aₜ$0) → (⊕ (a$1 ⟦A₂⟧)) → aₜ$0, Bₗ, Bᵣ}]]) : ∃ A₀' A₀'' A₁' A₁'' A₂' A₂'' Bₗ' Bᵣ', A₀ = A₀'.TypeVar_open a (n + 1) ∧ A₀ = A₀''.TypeVar_open a (n + 2) ∧ A₁ = A₁'.TypeVar_open a (n + 1) ∧ A₁ = A₁''.TypeVar_open a (n + 2) ∧ A₂ = A₂'.TypeVar_open a (n + 1) ∧ A₂ = A₂''.TypeVar_open a (n + 2) ∧ Bₗ = Bₗ'.TypeVar_open a n ∧ Bᵣ = Bᵣ'.TypeVar_open a n ∧ A = [[⊗ {∀ a : K ↦ *. (⊗ (a$0 ⟦A₀'⟧)) → (⊗ (a$0 ⟦A₁'⟧)) → ⊗ (a$0 ⟦A₂'⟧), ∀ a : K ↦ *. ∀ aₜ : *. ((⊕ (a$1 ⟦A₀''⟧)) → aₜ$0) → ((⊕ (a$1 ⟦A₁''⟧)) → aₜ$0) → (⊕ (a$1 ⟦A₂''⟧)) → aₜ$0, Bₗ', Bᵣ'}]] := by cases A <;> rw [TypeVar_open] at * case prod => rename «Type» => A let eq' := prod.inj eq cases A <;> rw [TypeVar_open] at * case list => rcases list.inj eq' with ⟨eq'', rfl⟩ rw [List.mapMem_eq_map] at * rename List _ => As match As with | [] => nomatch eq'' | A₀' :: As' => rw [List.map_cons] at * match As' with | [] => generalize A₀'.TypeVar_open a n = A₀'' at * nomatch eq'' | A₁' :: As'' => rw [List.map_cons] at * match As'' with | [] => generalize A₀'.TypeVar_open a n = A₀'' at * generalize A₁'.TypeVar_open a n = A₁'' at * nomatch eq'' | Bₗ' :: As'' => rw [List.map_cons] at * match As'' with | [] => generalize A₀'.TypeVar_open a n = A₀'' at * generalize A₁'.TypeVar_open a n = A₁'' at * generalize Bₗ'.TypeVar_open a n = Bₗ'' at * nomatch eq'' | Bᵣ' :: As'' => rw [List.map_cons] at * match As'' with | A₅' :: As'' => generalize A₀'.TypeVar_open a n = A₀'' at * generalize A₁'.TypeVar_open a n = A₁'' at * generalize Bₗ'.TypeVar_open a n = Bₗ'' at * generalize Bᵣ'.TypeVar_open a n = Bᵣ'' at * generalize A₅'.TypeVar_open a n = A₅'' at * nomatch eq'' | [] => rw [List.map_nil] at * let ⟨eq₀, eq'''⟩ := List.cons_eq_cons.mp eq'' let ⟨eq₁, eq''''⟩ := List.cons_eq_cons.mp eq''' let ⟨eq₂, eq'''''⟩ := List.cons_eq_cons.mp eq'''' let ⟨eq₃, _⟩ := List.cons_eq_cons.mp eq''''' cases A₀' <;> rw [TypeVar_open] at * case «forall» => let ⟨Keq, eq₀'⟩ := forall.inj eq₀ cases Keq rename «Type» => A₀' cases A₀' <;> rw [TypeVar_open] at * case arr => rename_i A₀₀' A₀₁' cases A₀₀' <;> rw [Type.TypeVar_open] at * case prod => rename «Type» => A₀₀' cases A₀₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₀₀₀' A₀₀₁' cases A₀₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₀₁' <;> rw [Type.TypeVar_open] at * case arr => rename_i A₀₁₀' A₀₁₁' cases A₀₁₀' <;> rw [Type.TypeVar_open] at * case prod => rename «Type» => A₀₁₀' cases A₀₁₀' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₀₁₀₀' A₀₁₀₁' cases A₀₁₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₀₁₁' <;> rw [Type.TypeVar_open] at * case prod => rename «Type» => A₀₁₁' cases A₀₁₁' <;> rw [Type.TypeVar_open] at * case listApp => rename_i A₀₁₁₀' A₀₁₁₁' cases A₀₁₁₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₁' <;> rw [TypeVar_open] at * case «forall» => let ⟨Keq, eq₁'⟩ := forall.inj eq₁ cases Keq rename «Type» => A₁' cases A₁' <;> rw [TypeVar_open] at * case «forall» => let ⟨Keq, eq₁''⟩ := forall.inj eq₁' cases Keq rename «Type» => A₁' cases A₁' <;> rw [TypeVar_open] at * case arr => rename_i A₁₀' A₁₁' cases A₁₀' <;> rw [TypeVar_open] at * case arr => rename_i A₁₀₀' A₁₀₁' cases A₁₀₀' <;> rw [TypeVar_open] at * case sum => rename «Type» => A₁₀₀' cases A₁₀₀' <;> rw [TypeVar_open] at * case listApp => rename_i A₁₀₀₀' A₁₀₀₁' cases A₁₀₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 1 => rw [if_neg nofun] at * cases A₁₀₁' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₁₁' <;> rw [Type.TypeVar_open] at * case arr => rename_i A₁₁₀' A₁₁₁' cases A₁₁₀' <;> rw [TypeVar_open] at * case arr => rename_i A₁₁₀₀' A₁₁₀₁' cases A₁₁₀₀' <;> rw [TypeVar_open] at * case sum => rename «Type» => A₁₁₀₀' cases A₁₁₀₀' <;> rw [TypeVar_open] at * case listApp => rename_i A₁₁₀₀₀' A₁₁₀₀₁' cases A₁₁₀₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 1 => rw [if_neg nofun] at * cases A₁₁₀₁' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases A₁₁₁' <;> rw [TypeVar_open] at * case arr => rename_i A₁₁₁₀' A₁₁₁₁' cases A₁₁₁₀' <;> rw [TypeVar_open] at * case sum => rename «Type» => A₁₁₁₀' cases A₁₁₁₀' <;> rw [TypeVar_open] at * case listApp => rename_i A₁₁₁₀₀' A₁₁₁₀₁' cases A₁₁₁₀₀' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 1 => rw [if_neg nofun] at * cases A₁₁₁₁' <;> rw [Type.TypeVar_open] at * case var => rename «F⊗⊕ω».TypeVar => a' cases a' case bound => rename Nat => n' match n' with | 0 => rw [if_neg nofun] at * cases eq₀' let ⟨eq₁₀, eq₁₁⟩ := arr.inj eq₁'' let ⟨eq₁₁₀, eq₁₁₁⟩ := arr.inj eq₁₁ exact ⟨ _, _, _, _, _, _, _, _, rfl, And.right <| listApp.inj <| sum.inj <| And.left <| arr.inj eq₁₀.symm, rfl, And.right <| listApp.inj <| sum.inj <| And.left <| arr.inj eq₁₁₀.symm, rfl, And.right <| listApp.inj <| sum.inj <| And.left <| arr.inj eq₁₁₁.symm, eq₂.symm, eq₃.symm, rfl ⟩ | _ + 1 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' | 0 | _ + 2 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' | _ + 1 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' | 0 | _ + 2 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' | _ + 1 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' | 0 | _ + 2 => split at eq₁'' <;> nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁'' all_goals nomatch eq₁' all_goals nomatch eq₁ | _ + 1 => split at eq₀' <;> nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' | _ + 1 => split at eq₀' <;> nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' | _ + 1 => split at eq₀' <;> nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀' all_goals nomatch eq₀ all_goals nomatch eq all_goals nomatch eq local instance : Inhabited «Type» where default := .list [] none in theorem tc_evidence_eq_inversion (aninA : a ∉ A.freeTypeVars) (A'oplc : (A'.TypeVar_open a').TypeVarLocallyClosed) (A''oplc : ∀ i ∈ [:n'], ((A'' i).TypeVar_open a').TypeVarLocallyClosed) (Blc : B.TypeVarLocallyClosed) (eq : A.TypeVar_open a n = [[⊗ {A'^^B, }]]) : ∃ A''' A'''', A'.Type_open B = A'''.TypeVar_open a n ∧ (∀ i ∈ [:n'], (A'' i).Type_open B = (A'''' i).TypeVar_open a n) ∧ A = [[⊗ {A''', }]] := by cases A <;> rw [TypeVar_open] at * case prod => rename «Type» => A let eq' := prod.inj eq cases A <;> rw [TypeVar_open] at * case list => rcases list.inj eq' with ⟨eq'', rfl⟩ rw [List.mapMem_eq_map] at * rename List _ => As match As with | [] => nomatch eq'' | A''' :: A'''' => rw [List.map_cons] at * let ⟨eq₀, eq₁⟩ := List.cons_eq_cons.mp eq'' rw [← Range.map_get!_eq (as := A''''), Range.map, List.map_map, ← Range.map] at eq₁ let length_eq : List.length (Range.map ..) = List.length _ := by rw [eq₁] rw [List.length_map, List.length_map, Range.length_toList, Range.length_toList, Nat.sub_zero, Nat.sub_zero] at length_eq cases length_eq rw [freeTypeVars, freeTypeVars, List.mapMem_eq_map, List.map_cons, List.flatten] at aninA let ⟨aninA'', aninA''''⟩ := List.not_mem_append'.mp aninA let A'lc := A'oplc.weaken (n := 1).TypeVar_open_drop <| Nat.lt.base _ let A'opBlc := A'lc.Type_open_dec Blc |>.weaken (n := n) rw [Nat.zero_add] at A'opBlc rw [← A'opBlc.TypeVar_open_TypeVar_close_id (a := a)] at eq₀ cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars aninA'' Type.not_mem_freeTypeVars_TypeVar_close eq₀ let A'lc' := A'lc.weaken (n := n) rw [Nat.add_comm] at A'lc' apply Exists.intro <| (A'.Type_open B).TypeVar_close a n apply Exists.intro fun i => ((A''''.get! i).TypeVar_open a n).TypeVar_close a n constructor · exact A'opBlc.TypeVar_open_TypeVar_close_id (a := a).symm · constructor · intro i mem let A''eq := Range.eq_of_mem_of_map_eq eq₁ i mem simp only [Function.comp] at A''eq ⊢ let A''oplc' := A''oplc i mem |>.weaken (n := 1).TypeVar_open_drop <| Nat.lt.base _ let A''opBlc := A''oplc'.Type_open_dec Blc |>.weaken (n := n) rw [Nat.zero_add] at A''opBlc rw [← A''opBlc.TypeVar_open_TypeVar_close_id (a := a), A''eq] · congr rw (occs := .pos [1]) [← Range.map_get!_eq (as := A'''')] apply Range.map_eq_of_eq_of_mem intro i mem symm apply Type.TypeVar_close_TypeVar_open_eq_of_not_mem_freeTypeVars exact List.not_mem_flatten.mp aninA'''' (A''''.get! i).freeTypeVars <| List.mem_map.mpr ⟨_, List.get!_mem mem.upper, rfl⟩ all_goals nomatch eq all_goals nomatch eq private theorem ind_evidence_inversion (eq : A.TypeVar_open a n = [[∀ aₘ : (L K) ↦ *. (∀ aₗ : *. ∀ aₜ : K. ∀ aₚ : L K. ∀ aᵢ : L K. ∀ aₙ : L K. Bₗ → Bᵣ → (⊗ { : * }) → (aₘ$5 aₚ$2) → aₘ$5 aᵢ$1) → (aₘ$0 { : K }) → aₘ$0 A']]) : ∃ Bₗ' Bᵣ' A'', Bₗ = Bₗ'.TypeVar_open a (n + 6) ∧ Bᵣ = Bᵣ'.TypeVar_open a (n + 6) ∧ A' = A''.TypeVar_open a (n + 1) ∧ A = [[∀ aₘ : (L K) ↦ *. (∀ aₗ : *. ∀ aₜ : K. ∀ aₚ : L K. ∀ aᵢ : L K. ∀ aₙ : L K. Bₗ' → Bᵣ' → (⊗ { : * }) → (aₘ$5 aₚ$2) → aₘ$5 aᵢ$1) → (aₘ$0 { : K }) → aₘ$0 A'']] := by cases A <;> rw [TypeVar_open] at eq case «forall» A => rcases forall.inj eq with ⟨rfl, eq'⟩ cases A <;> rw [TypeVar_open] at eq' case arr A₀ A₁ => let ⟨eq₀, eq₁⟩ := arr.inj eq' cases A₀ <;> rw [TypeVar_open] at eq₀ case «forall» A₀ => rcases forall.inj eq₀ with ⟨rfl, eq₀'⟩ cases A₀ <;> rw [TypeVar_open] at eq₀' case «forall» A₀ => rcases forall.inj eq₀' with ⟨rfl, eq₀''⟩ cases A₀ <;> rw [TypeVar_open] at eq₀'' case «forall» A₀ => rcases forall.inj eq₀'' with ⟨rfl, eq₀'''⟩ cases A₀ <;> rw [TypeVar_open] at eq₀''' case «forall» A₀ => rcases forall.inj eq₀''' with ⟨rfl, eq₀''''⟩ cases A₀ <;> rw [TypeVar_open] at eq₀'''' case «forall» A₀ => rcases forall.inj eq₀'''' with ⟨rfl, eq₀'''''⟩ cases A₀ <;> rw [TypeVar_open] at eq₀''''' case arr Bₗ' A₀ => let ⟨Bₗeq, eq₀''''''⟩ := arr.inj eq₀''''' cases A₀ <;> rw [TypeVar_open] at eq₀'''''' case arr Bᵣ' A₀ => let ⟨Bᵣeq, eq₀'''''''⟩ := arr.inj eq₀'''''' cases A₀ <;> rw [TypeVar_open] at eq₀''''''' case arr A₀₀ A₀₁ => let ⟨eq₀₀, eq₀₁⟩ := arr.inj eq₀''''''' cases A₀₀ <;> rw [TypeVar_open] at eq₀₀ case prod A₀₀ => let eq₀₀' := prod.inj eq₀₀ cases A₀₀ <;> rw [TypeVar_open] at eq₀₀' case list => rcases list.inj eq₀₀' with ⟨eq₀₀'', rfl⟩ rw [List.mapMem_eq_map] at eq₀₀'' cases List.map_eq_nil_iff.mp eq₀₀'' cases A₀₁ <;> rw [TypeVar_open] at eq₀₁ case arr A₀₁₀ A₀₁₁ => let ⟨eq₀₁₀, eq₀₁₁⟩ := arr.inj eq₀₁ cases A₀₁₀ <;> rw [TypeVar_open] at eq₀₁₀ case app A₀₁₀₀ A₀₁₀₁ => let ⟨eq₀₁₀₀, eq₀₁₀₁⟩ := app.inj eq₀₁₀ cases A₀₁₀₀ <;> rw [TypeVar_open] at eq₀₁₀₀ case var a' => match a' with | .bound n' => split at eq₀₁₀₀ · case isTrue => nomatch eq₀₁₀₀ · case isFalse => cases eq₀₁₀₀ cases A₀₁₀₁ <;> rw [TypeVar_open] at eq₀₁₀₁ case var a' => match a' with | .bound n' => split at eq₀₁₀₁ · case isTrue => nomatch eq₀₁₀₁ · case isFalse => cases eq₀₁₀₁ cases A₀₁₁ <;> rw [TypeVar_open] at eq₀₁₁ case app A₀₁₁₀ A₀₁₁₁ => let ⟨eq₀₁₁₀, eq₀₁₁₁⟩ := app.inj eq₀₁₁ cases A₀₁₁₀ <;> rw [TypeVar_open] at eq₀₁₁₀ case var a' => match a' with | .bound n' => split at eq₀₁₁₀ · case isTrue => nomatch eq₀₁₁₀ · case isFalse => cases eq₀₁₁₀ cases A₀₁₁₁ <;> rw [TypeVar_open] at eq₀₁₁₁ case var a' => match a' with | .bound n' => split at eq₀₁₁₁ · case isTrue => nomatch eq₀₁₁₁ · case isFalse => cases eq₀₁₁₁ cases A₁ <;> rw [TypeVar_open] at eq₁ case arr A₁₀ A₁₁ => let ⟨eq₁₀, eq₁₁⟩ := arr.inj eq₁ cases A₁₀ <;> rw [TypeVar_open] at eq₁₀ case app A₁₀₀ A₁₀₁ => let ⟨eq₁₀₀, eq₁₀₁⟩ := app.inj eq₁₀ cases A₁₀₀ <;> rw [TypeVar_open] at eq₁₀₀ case var a' => match a' with | .bound n' => split at eq₁₀₀ · case isTrue => nomatch eq₁₀₀ · case isFalse => cases eq₁₀₀ cases A₁₀₁ <;> rw [TypeVar_open] at eq₁₀₁ case list A₁₀₁ => rcases list.inj eq₁₀₁ with ⟨eq₁₀₁', rfl⟩ rw [List.mapMem_eq_map] at eq₁₀₁' cases List.map_eq_nil_iff.mp eq₁₀₁' cases A₁₁ <;> rw [TypeVar_open] at eq₁₁ case app A₁₁₀ A'' => let ⟨eq₁₁₀, A'eq⟩ := app.inj eq₁₁ cases A₁₁₀ <;> rw [TypeVar_open] at eq₁₁₀ case var a' => match a' with | .bound n' => split at eq₁₁₀ · case isTrue => nomatch eq₁₁₀ · case isFalse => cases eq₁₁₀ exact ⟨_, _, _, Bₗeq.symm, Bᵣeq.symm, A'eq.symm, rfl⟩ | .free _ => split at eq₁₁₀ <;> nomatch eq₁₁₀ all_goals nomatch eq₁₁₀ all_goals nomatch eq₁₁ all_goals nomatch eq₁₀₁ | .free _ => split at eq₁₀₀ <;> nomatch eq₁₀₀ all_goals nomatch eq₁₀₀ all_goals nomatch eq₁₀ all_goals nomatch eq₁ | .free _ => split at eq₀₁₁₁ <;> nomatch eq₀₁₁₁ all_goals nomatch eq₀₁₁₁ | .free _ => split at eq₀₁₁₀ <;> nomatch eq₀₁₁₀ all_goals nomatch eq₀₁₁₀ all_goals nomatch eq₀₁₁ | .free _ => split at eq₀₁₀₁ <;> nomatch eq₀₁₀₁ all_goals nomatch eq₀₁₀₁ | .free _ => split at eq₀₁₀₀ <;> nomatch eq₀₁₀₀ all_goals nomatch eq₀₁₀₀ all_goals nomatch eq₀₁₀ all_goals nomatch eq₀₁ all_goals nomatch eq₀₀' all_goals nomatch eq₀₀ all_goals nomatch eq₀''''''' all_goals nomatch eq₀'''''' all_goals nomatch eq₀''''' all_goals nomatch eq₀'''' all_goals nomatch eq₀''' all_goals nomatch eq₀'' all_goals nomatch eq₀' all_goals nomatch eq₀ all_goals nomatch eq' all_goals nomatch eq end «F⊗⊕ω».Type open «F⊗⊕ω» local instance : Inhabited Monotype where default := .row [] none in local instance : Inhabited «Type» where default := .list [] none in set_option maxHeartbeats 2000000 in open TypeScheme in mutual theorem TypeScheme.KindingAndElaboration.Monotype_open_preservation (σke : KindingAndElaboration Γc [[Γ, a : κ₀, Γ']] (TypeVar_open σ a m) κ₁ (Type.TypeVar_open A a n)) (Γcw : [[⊢c Γc]]) (ΓaΓ'we : [[Γc ⊢ Γ, a : κ₀, Γ' ⇝ Δ]]) (aninΓ' : [[a ∉ dom(Γ')]]) (aninσ : a ∉ σ.freeTypeVars) (aninA : a ∉ A.freeTypeVars) (τke : [[Γc; Γ ⊢ τ : κ₀ ⇝ B]]) : KindingAndElaboration Γc [[Γ, (Γ' [τ / a])]] (σ.Monotype_open τ m) κ₁ (A.Type_open B n) := open KindingAndElaboration in by let .qual (.mono τlc) := τke.TypeVarLocallyClosed_of match σ with | .qual γ => rw [Monotype_open] rw [TypeVar_open] at σke rw [freeTypeVars] at aninσ match h : γ with | .mono τ' => rw [QualifiedType.Monotype_open] rw [QualifiedType.TypeVar_open] at σke rw [QualifiedType.freeTypeVars] at aninσ match τ' with | .var _ => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case var => split at σke · case isTrue h => cases h split at σke · case isTrue h => cases h rw [Monotype.Monotype_open, if_pos rfl, Type.Type_open, if_pos rfl] let .var ain := σke let .head := ain.append_elim_left aninΓ' let ⟨_, κ₁e⟩ := κ₁.Elaboration_total let ainΔ := ΓaΓ'we.TypeVarIn_preservation ain κ₁e rcases ainΔ.eq_of with ⟨_, _, rfl⟩ exact τke.weakening (Γ'' := .empty) <| ΓaΓ'we.TypeVar_subst_preservation Γcw aninΓ' τke · case isFalse h => let .var .. := σke rw [Type.freeTypeVars] at aninA nomatch List.not_mem_singleton.mp aninA · case isFalse h => split at σke · case isTrue h' => cases h' let .var .. := σke rw [Monotype.freeTypeVars] at aninσ nomatch List.not_mem_singleton.mp aninσ · case isFalse h' => rw [Monotype.Monotype_open, if_neg h, Type.Type_open, if_neg h'] let .var a'in := σke rw [Type.freeTypeVars] at aninA exact var <| match a'in.append_elim with | .inl ⟨a'inΓa, a'ninΓ'⟩ => match a'inΓa with | .head => nomatch List.not_mem_singleton.mp aninA | .typeExt _ a'inΓ => a'inΓ.append_inl a'ninΓ'.TypeVar_subst_preservation | .inr a'inΓ' => a'inΓ'.TypeVar_subst_preservation.append_inr all_goals split at σke <;> nomatch σke | .app ϕ τ'' => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case app => let .app ϕke τ''ke := σke rw [Monotype.Monotype_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at ϕke τ''ke rw [Monotype.freeTypeVars] at aninσ rw [Type.freeTypeVars] at aninA let ϕke' := ϕke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_left _ ·) (aninA <| List.mem_append_left _ ·) τke let τ''ke' := τ''ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) (aninA <| List.mem_append_right _ ·) τke rw [Monotype_open, QualifiedType.Monotype_open] at ϕke' τ''ke' exact app ϕke' τ''ke' all_goals nomatch σke | .arr τ₀ τ₁ => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case arr => let .arr τ₀ke τ₁ke := σke rw [Monotype.Monotype_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at τ₀ke τ₁ke rw [Monotype.freeTypeVars] at aninσ rw [Type.freeTypeVars] at aninA let τ₀ke' := τ₀ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_left _ ·) (aninA <| List.mem_append_left _ ·) τke let τ₁ke' := τ₁ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) (aninA <| List.mem_append_right _ ·) τke rw [Monotype_open, QualifiedType.Monotype_open] at τ₀ke' τ₁ke' exact arr τ₀ke' τ₁ke' all_goals nomatch σke | .label _ => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case prod => rw [Monotype.Monotype_open, Type.Type_open] rename «Type» => A cases A <;> rw [Type.TypeVar_open] at σke case list => rw [Type.Type_open] rw [List.mapMem_eq_map] at σke ⊢ rename List _ => As match As with | _ :: _ => nomatch σke | [] => rw [List.map_nil] at σke ⊢ let .label := σke exact label all_goals nomatch σke all_goals nomatch σke | .comm _ => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case prod => rw [Monotype.Monotype_open, Type.Type_open] rename «Type» => A cases A <;> rw [Type.TypeVar_open] at σke case list => rw [Type.Type_open] rw [List.mapMem_eq_map] at σke ⊢ rename List _ => As match As with | _ :: _ => nomatch σke | [] => rw [List.map_nil] at σke ⊢ let .comm := σke exact comm all_goals nomatch σke all_goals nomatch σke | .row ξτs .. => rw [Monotype.TypeVar_open, List.mapMem_eq_map] at σke generalize ξτs'eq : (ξτs.map fun (ξ, τ) => (ξ.TypeVar_open a m, τ.TypeVar_open a m)) = ξτs' at σke generalize A'eq : A.TypeVar_open a n = A' at σke let .row ξ'ke uni τ'ke κ'e h' := σke rename_i B' _ _ _ _ _ _ _ cases A <;> rw [Type.TypeVar_open] at A'eq case list => rename List _ => A rw [List.mapMem_eq_map] at A'eq rcases Type.list.inj A'eq with ⟨A'eq', rfl⟩ let ξτslength_eq : List.length (List.map ..) = List.length _ := by rw [ξτs'eq] let Alength_eq : List.length (List.map ..) = List.length _ := by rw [A'eq'] rw [List.length_map, List.length_map, Range.length_toList, Nat.sub_zero] at ξτslength_eq Alength_eq let ξ' i := ξτs.get! i |>.fst.Monotype_open τ m let τ' i := ξτs.get! i |>.snd.Monotype_open τ m let A'' i := A.get! i |>.Type_open B n rw [Monotype.Monotype_open, List.mapMem_eq_map, ← Range.map_get!_eq (as := ξτs), ξτslength_eq, Range.map, List.map_map, Type.Type_open, List.mapMem_eq_map, ← Range.map_get!_eq (as := A), Alength_eq, Range.map, List.map_map, Range.map_eq_of_eq_of_mem (by intro i _ show _ = (ξ' i, τ' i) simp only [Function.comp, ξ', τ'] ), ← Range.map, Range.map_eq_of_eq_of_mem (by intro i _ show _ = A'' i simp only [Function.comp, A''] ), ← Range.map] rw [← Range.map_get!_eq (as := ξτs), ξτslength_eq, Range.map, List.map_map] at ξτs'eq rw [Monotype.freeTypeVars, List.mapMem_eq_map] at aninσ let aninξ i ilt : a ∉ (ξτs.get! i).fst.freeTypeVars := by apply (List.not_mem_append' (ys := (ξτs.get! i).snd.freeTypeVars)).mp _ |>.left apply List.not_mem_flatten.mp aninσ apply List.mem_map.mpr exact ⟨_, List.get!_mem ilt, rfl⟩ let aninτ i ilt : a ∉ (ξτs.get! i).snd.freeTypeVars := by apply (List.not_mem_append' (xs := (ξτs.get! i).fst.freeTypeVars)).mp _ |>.right apply List.not_mem_flatten.mp aninσ apply List.mem_map.mpr exact ⟨_, List.get!_mem ilt, rfl⟩ apply row _ _ _ κ'e h' · exact fun i => ((B' i).TypeVar_close a m).Type_open B m · intro i mem dsimp only [ξ'] let ξike := ξ'ke i mem simp only at ξike have := Range.eq_of_mem_of_map_eq ξτs'eq i mem simp only [Function.comp] at this rw [← Prod.mk.inj this |>.left, ← QualifiedType.TypeVar_open, ← TypeVar_open] at ξike let Bki := ξike.soundness Γcw ΓaΓ'we .label |>.TypeVarLocallyClosed_of.weaken (n := m) rw [Nat.zero_add] at Bki rw [← Bki.TypeVar_open_TypeVar_close_id (a := a)] at ξike let ilt : i < ξτs.length := by rw [ξτslength_eq]; exact mem.upper have := ξike.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninξ i ilt) Type.not_mem_freeTypeVars_TypeVar_close τke rw [Monotype_open, QualifiedType.Monotype_open] at this exact this · rw [funext (f := fun i => ξ' i) (by intro i show _ = ((fun x => x.Monotype_open τ m) ∘ (fun i => ξτs.get! i |>.fst)) i simp only [ξ', Function.comp] ), Range.map, ← List.map_map] apply Monotype.label.Uniqueness.Monotype_open_preservation (a := a) rw [Range.map, Range.map_eq_of_eq_of_mem (by intro i mem have := Range.eq_of_mem_of_map_eq ξτs'eq i mem simp only [Function.comp] at this rw [← Prod.mk.inj this |>.left] )] at uni rw [List.map_map, ← Range.map, Range.map, Range.map_eq_of_eq_of_mem (by intro i mem show _ = (ξτs.get! i).fst.TypeVar_open a m simp only [Function.comp] )] exact uni · intro i mem dsimp only [τ', A''] let τike := τ'ke i mem simp only at τike have := Range.eq_of_mem_of_map_eq ξτs'eq i mem simp only [Function.comp] at this rw [← Prod.mk.inj this |>.right, ← QualifiedType.TypeVar_open, ← TypeVar_open] at τike rw [← Range.map_get!_eq (as := A), Range.map, List.map_map, Alength_eq] at A'eq' have := Range.eq_of_mem_of_map_eq A'eq' i mem simp only [Function.comp] at this rw [← this] at τike rw [Type.freeTypeVars, List.mapMem_eq_map] at aninA have iltAlength : i < A.length := by rw [Alength_eq] exact mem.upper let aninAi := List.not_mem_flatten.mp aninA (A.get! i).freeTypeVars (List.mem_map.mpr ⟨_, List.get!_mem iltAlength, rfl⟩) let ilt : i < ξτs.length := by rw [ξτslength_eq]; exact mem.upper have := τike.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninτ i ilt) aninAi τke rw [Monotype_open, QualifiedType.Monotype_open] at this exact this all_goals nomatch A'eq | .floor _ => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case prod => rw [Monotype.Monotype_open, Type.Type_open] rename «Type» => A cases A <;> rw [Type.TypeVar_open] at σke case list => rw [Type.Type_open] rw [List.mapMem_eq_map] at σke ⊢ rename List _ => As match As with | _ :: _ => nomatch σke | [] => rw [List.map_nil] at σke ⊢ let .floor ξke := σke rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at ξke let Alc := ξke.soundness Γcw ΓaΓ'we .label |>.TypeVarLocallyClosed_of.weaken (n := n) rw [Nat.zero_add] at Alc rw [← Alc.TypeVar_open_TypeVar_close_id (a := a)] at ξke rw [Monotype.freeTypeVars] at aninσ exact floor <| ξke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninσ Type.not_mem_freeTypeVars_TypeVar_close τke all_goals nomatch σke all_goals nomatch σke | .prodOrSum .prod .. => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case prod => let .prod μke ρke := σke rw [Monotype.Monotype_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at μke ρke rw [Monotype.freeTypeVars] at aninσ rw [Type.freeTypeVars] at aninA let Blc := μke.soundness Γcw ΓaΓ'we .comm |>.TypeVarLocallyClosed_of.weaken (n := n) rw [Nat.zero_add] at Blc rw [← Blc.TypeVar_open_TypeVar_close_id (a := a)] at μke let μke' := μke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_left _ ·) Type.not_mem_freeTypeVars_TypeVar_close τke let ρke' := ρke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) aninA τke rw [Monotype_open, QualifiedType.Monotype_open] at μke' ρke' exact prod μke' ρke' all_goals nomatch σke | .prodOrSum .sum .. => rw [Monotype.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case sum => let .sum μke ρke := σke rw [Monotype.Monotype_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at μke ρke rw [Monotype.freeTypeVars] at aninσ rw [Type.freeTypeVars] at aninA let Blc := μke.soundness Γcw ΓaΓ'we .comm |>.TypeVarLocallyClosed_of.weaken (n := n) rw [Nat.zero_add] at Blc rw [← Blc.TypeVar_open_TypeVar_close_id (a := a)] at μke let μke' := μke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_left _ ·) Type.not_mem_freeTypeVars_TypeVar_close τke let ρke' := ρke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) aninA τke rw [Monotype_open, QualifiedType.Monotype_open] at μke' ρke' exact sum μke' ρke' all_goals nomatch σke | .lift .. => rename TypeLambda => «λτ» let .mk _ τ'' := «λτ» rw [Monotype.TypeVar_open, TypeLambda.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case listApp => rename_i A _ cases A <;> rw [Type.TypeVar_open] at σke case lam => rename «Type» => A let .lift I τ''ke κ₀'e ρke := σke rw [Monotype.Monotype_open, TypeLambda.Monotype_open, Type.Type_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at ρke rw [Monotype.freeTypeVars, TypeLambda.freeTypeVars] at aninσ rw [Type.freeTypeVars, Type.freeTypeVars] at aninA let ρke' := ρke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) (aninA <| List.mem_append_right _ ·) τke rw [Monotype_open, QualifiedType.Monotype_open] at ρke' apply lift ([[(Γ, a : κ₀, Γ')]].typeVarDom ++ I) _ κ₀'e ρke' intro a' a'nin let ⟨a'ninΓaΓ'', a'ninI⟩ := List.not_mem_append'.mp a'nin have a'ninΓa : [[a' ∉ dom(Γ, a : κ₀)]] := by rw [TypeEnvironment.typeVarDom_append] at a'ninΓaΓ'' exact List.not_mem_append'.mp a'ninΓaΓ'' |>.right let ne := List.ne_of_not_mem_cons a'ninΓa symm at ne let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [Blc.Type_open_TypeVar_open_comm <| Nat.succ_ne_zero _] have := τ''ke a' a'ninI rw [τ''.TypeVar_open_comm <| Nat.succ_ne_zero _, ← QualifiedType.TypeVar_open, ← TypeVar_open, A.TypeVar_open_comm <| Nat.succ_ne_zero _, ← TypeEnvironment.append] at this have := this.Monotype_open_preservation Γcw (ΓaΓ'we.typeExt a'ninΓaΓ'' κ₀'e) (List.not_mem_cons.mpr ⟨ne, aninΓ'⟩) (Monotype.not_mem_freeTypeVars_TypeVar_open_intro (aninσ <| List.mem_append_left _ ·) ne) (Type.not_mem_freeTypeVars_TypeVar_open_intro (aninA <| List.mem_append_left _ ·) ne) τke rw [← TypeEnvironment.append, ← TypeEnvironment.TypeVar_subst, ← τ''.TypeVar_open_Monotype_open_comm τlc <| Nat.zero_ne_add_one _, ← QualifiedType.Monotype_open, ← Monotype_open] exact this all_goals nomatch σke all_goals nomatch σke | .contain .. => rw [Monotype.TypeVar_open] at σke generalize A'eq : A.TypeVar_open a n = A' at σke let .contain μke ρ₀ke ρ₁ke κe := σke let ⟨A₀, A₁, eq₀, eq₁, eq₂⟩ := Type.contain_evidence_eq_inversion aninA A'eq cases eq₀ cases eq₁ cases eq₂ clear A'eq rw [Monotype.Monotype_open, Type.Type_open, Type.Type_open, List.mapMem_eq_map, List.map_cons, List.map_singleton] repeat rw [Type.Type_open] rw [if_neg nofun] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at μke ρ₀ke ρ₁ke rw [Monotype.freeTypeVars] at aninσ let ⟨aninρ₀μ, aninρ₁⟩ := List.not_mem_append'.mp aninσ let ⟨aninρ₀, aninμ⟩ := List.not_mem_append'.mp aninρ₀μ simp [Type.freeTypeVars] at aninA let ⟨_, aninA₀, aninA₁⟩ := aninA let Blc := μke.soundness Γcw ΓaΓ'we .comm |>.TypeVarLocallyClosed_of.weaken (n := n) rw [Nat.zero_add] at Blc rw [← Blc.TypeVar_open_TypeVar_close_id (a := a)] at μke let μke' := μke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninμ Type.not_mem_freeTypeVars_TypeVar_close τke let ρ₀ke' := ρ₀ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninρ₀ aninA₀ τke let ρ₁ke' := ρ₁ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninρ₁ aninA₁ τke rw [Monotype_open, QualifiedType.Monotype_open] at ρ₀ke' ρ₁ke' exact contain μke' ρ₀ke' ρ₁ke' κe | .concat .. => rw [Monotype.TypeVar_open] at σke generalize A'eq : A.TypeVar_open a n = A' at σke let .concat μke ρ₀ke ρ₁ke ρ₂ke κe keBₗ keBᵣ := σke rcases Type.concat_evidence_eq_inversion A'eq with ⟨A₀', A₀'', A₁', A₁'', A₂', A₂'', Bₗ', Bᵣ', eq₀, eq₀', eq₁, eq₁', eq₂, eq₂', rfl, rfl, rfl⟩ simp [Type.Type_open] rw [Monotype.Monotype_open] simp [Type.freeTypeVars] at aninA let ⟨aninA₀', aninA₁', aninA₂', aninA₀'', aninA₁'', aninA₂'', aninBₗ', aninBᵣ'⟩:= aninA let A₀lc := ρ₀ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 1) let A₀lc' := ρ₀ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 2) rw [Nat.zero_add] at A₀lc A₀lc' rw [← A₀lc.TypeVar_open_TypeVar_close_id (a := a)] at eq₀ ρ₀ke rw [← A₀lc'.TypeVar_open_TypeVar_close_id (a := a)] at eq₀' cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₀' eq₀ cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₀'' eq₀' let A₁lc := ρ₁ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 1) let A₁lc' := ρ₁ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 2) rw [Nat.zero_add] at A₁lc A₁lc' rw [← A₁lc.TypeVar_open_TypeVar_close_id (a := a)] at eq₁ ρ₁ke rw [← A₁lc'.TypeVar_open_TypeVar_close_id (a := a)] at eq₁' cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₁' eq₁ cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₁'' eq₁' let A₂lc := ρ₂ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 1) let A₂lc' := ρ₂ke.soundness Γcw ΓaΓ'we κe.row |>.TypeVarLocallyClosed_of.weaken (n := n + 2) rw [Nat.zero_add] at A₂lc A₂lc' rw [← A₂lc.TypeVar_open_TypeVar_close_id (a := a)] at eq₂ ρ₂ke rw [← A₂lc'.TypeVar_open_TypeVar_close_id (a := a)] at eq₂' cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₂' eq₂ cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA₂'' eq₂' rw [A₀lc'.Type_open_TypeVar_close_eq_TypeVar_subst, ← A₀lc.Type_open_TypeVar_close_eq_TypeVar_subst, A₁lc'.Type_open_TypeVar_close_eq_TypeVar_subst, ← A₁lc.Type_open_TypeVar_close_eq_TypeVar_subst, A₂lc'.Type_open_TypeVar_close_eq_TypeVar_subst, ← A₂lc.Type_open_TypeVar_close_eq_TypeVar_subst] simp [Monotype.freeTypeVars] at aninσ let ⟨aninρ₀, aninμ, aninρ₁, aninρ₂⟩ := aninσ rw [← Monotype.TypeVar_open] at keBₗ keBᵣ rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at μke ρ₀ke ρ₁ke ρ₂ke keBₗ keBᵣ let Blc := μke.soundness Γcw ΓaΓ'we .comm |>.TypeVarLocallyClosed_of.weaken (n := n) rw [Nat.zero_add] at Blc rw [← Blc.TypeVar_open_TypeVar_close_id (a := a)] at μke let μke' := μke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninμ Type.not_mem_freeTypeVars_TypeVar_close τke let ρ₀ke' := ρ₀ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninρ₀ Type.not_mem_freeTypeVars_TypeVar_close τke let ρ₁ke' := ρ₁ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninρ₁ Type.not_mem_freeTypeVars_TypeVar_close τke let ρ₂ke' := ρ₂ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninρ₂ Type.not_mem_freeTypeVars_TypeVar_close τke let keBₗ' := keBₗ.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (by simp [freeTypeVars, QualifiedType.freeTypeVars, Monotype.freeTypeVars] exact ⟨aninρ₀, aninμ, aninρ₂⟩) aninBₗ' τke let keBᵣ' := keBᵣ.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (by simp [freeTypeVars, QualifiedType.freeTypeVars, Monotype.freeTypeVars] exact ⟨aninρ₁, aninμ, aninρ₂⟩) aninBᵣ' τke rw [Monotype_open, QualifiedType.Monotype_open, Monotype.Monotype_open] at keBₗ' keBᵣ' exact concat μke' ρ₀ke' ρ₁ke' ρ₂ke' κe keBₗ' keBᵣ' | .typeClass .. => rw [Monotype.TypeVar_open] at σke generalize A'eq : A.TypeVar_open a n = A' at σke let .tc inΓc τ'ke (κ := κ) (A := A) (TC' := TC') (A' := A'') (n := n') (m := m) (σ := σ') (B := B') := σke let ⟨a', a'nin⟩ := a :: ↑A.freeTypeVars ++ ↑([:n'].map fun i => (A'' i).freeTypeVars).flatten |>.exists_fresh let ⟨_, κe, _, Aki, _, A''ki⟩ := Γcw.In_inversion inΓc let B'lc := τ'ke.soundness Γcw ΓaΓ'we κe |>.TypeVarLocallyClosed_of rcases Type.tc_evidence_eq_inversion aninA (Aki a').TypeVarLocallyClosed_of (A''ki a' · · |>.TypeVarLocallyClosed_of) B'lc A'eq with ⟨A', A''', eq₀, eq₁, rfl⟩ let Alc := Aki a' |>.TypeVarLocallyClosed_of.weaken (n := 1).TypeVar_open_drop Nat.one_pos rw [Type.freeTypeVars, Type.freeTypeVars, List.mapMem_eq_map, List.map_cons, List.flatten_cons, List.map_map] at aninA let ⟨aninA', aninA'''⟩ := List.not_mem_append'.mp aninA let AopB'lc := Alc.Type_open_dec B'lc let AopB'lc' := AopB'lc.weaken (n := n) rw [Nat.zero_add] at AopB'lc' rw [← AopB'lc'.TypeVar_open_TypeVar_close_id (a := a)] at eq₀ cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA' eq₀ let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [Type.Type_open, Type.Type_open, List.mapMem_eq_map, List.map_cons, List.map_map, Range.map_eq_of_eq_of_mem (by intro i mem show _ = ((A'' i).TypeVar_subst a B).Type_open (B'.TypeVar_subst a B) let A''eq := eq₁ i mem let A''lc := A''ki a' i mem |>.TypeVarLocallyClosed_of.weaken (n := 1).TypeVar_open_drop Nat.one_pos let A''opB'lc := A''lc.Type_open_dec B'lc let A''opB'lc' := A''opB'lc.weaken (n := n) rw [Nat.zero_add] at A''opB'lc' rw [← A''opB'lc'.TypeVar_open_TypeVar_close_id (a := a)] at A''eq let aninA'''' := List.not_mem_flatten.mp aninA''' (A''' i).freeTypeVars <| Range.mem_map_of_mem mem have := Type.TypeVar_open_inj_of_not_mem_freeTypeVars Type.not_mem_freeTypeVars_TypeVar_close aninA'''' A''eq rw [Function.comp, ← this, A''opB'lc'.Type_open_TypeVar_close_eq_TypeVar_subst, Blc.Type_open_TypeVar_subst_dist] ), AopB'lc'.Type_open_TypeVar_close_eq_TypeVar_subst, Blc.Type_open_TypeVar_subst_dist, Monotype.Monotype_open] let B'lc' := B'lc.weaken (n := n) rw [Nat.zero_add] at B'lc' rw [← QualifiedType.TypeVar_open, ← TypeVar_open, ← B'lc'.TypeVar_open_TypeVar_close_id (a := a)] at τ'ke rw [Monotype.freeTypeVars] at aninσ let τ'ke' := τ'ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninσ Type.not_mem_freeTypeVars_TypeVar_close τke rw [B'lc'.Type_open_TypeVar_close_eq_TypeVar_subst] at τ'ke' apply tc _ τ'ke' (TC' := TC') (m := m) (σ := σ') let ⟨a'nea, _⟩ := List.not_mem_cons.mp a'nin let aninA := Type.not_mem_freeTypeVars_TypeVar_open_drop <| (Aki a').not_mem_freeTypeVars_of <| List.not_mem_singleton.mpr a'nea.symm rw [Type.TypeVar_subst_id_of_not_mem_freeTypeVars aninA, Range.map_eq_of_eq_of_mem'' (by intro i mem show _ = ClassEnvironmentEntrySuper.mk (TC' i) (A'' i) let aninA'' := Type.not_mem_freeTypeVars_TypeVar_open_drop <| A''ki a' i mem |>.not_mem_freeTypeVars_of <| List.not_mem_singleton.mpr a'nea.symm rw [Type.TypeVar_subst_id_of_not_mem_freeTypeVars aninA''] )] exact inΓc | .all .. => rename TypeLambda => «λτ» let .mk _ ψ := «λτ» rw [Monotype.TypeVar_open, TypeLambda.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case prod => rename «Type» => A cases A <;> rw [Type.TypeVar_open] at σke case listApp => rename_i A _ cases A <;> rw [Type.TypeVar_open] at σke case lam => rename «Type» => A let .all I ψke κe ρke := σke rw [Monotype.Monotype_open, TypeLambda.Monotype_open, Type.Type_open, Type.Type_open, Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at ρke rw [Monotype.freeTypeVars, TypeLambda.freeTypeVars] at aninσ rw [Type.freeTypeVars, Type.freeTypeVars, Type.freeTypeVars] at aninA let ρke' := ρke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) (aninA <| List.mem_append_right _ ·) τke rw [Monotype_open, QualifiedType.Monotype_open] at ρke' apply all ([[(Γ, a : κ₀, Γ')]].typeVarDom ++ I) _ κe ρke' intro a' a'nin let ⟨a'ninΓaΓ'', a'ninI⟩ := List.not_mem_append'.mp a'nin have a'ninΓa : [[a' ∉ dom(Γ, a : κ₀)]] := by rw [TypeEnvironment.typeVarDom_append] at a'ninΓaΓ'' exact List.not_mem_append'.mp a'ninΓaΓ'' |>.right let ne := List.ne_of_not_mem_cons a'ninΓa symm at ne let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [Blc.Type_open_TypeVar_open_comm <| Nat.succ_ne_zero _] have := ψke a' a'ninI rw [ψ.TypeVar_open_comm <| Nat.succ_ne_zero _, ← QualifiedType.TypeVar_open, ← TypeVar_open, A.TypeVar_open_comm <| Nat.succ_ne_zero _, ← TypeEnvironment.append] at this have := this.Monotype_open_preservation Γcw (ΓaΓ'we.typeExt a'ninΓaΓ'' κe) (List.not_mem_cons.mpr ⟨ne, aninΓ'⟩) (Monotype.not_mem_freeTypeVars_TypeVar_open_intro (aninσ <| List.mem_append_left _ ·) ne) (Type.not_mem_freeTypeVars_TypeVar_open_intro (aninA <| List.mem_append_left _ ·) ne) τke rw [← TypeEnvironment.append, ← TypeEnvironment.TypeVar_subst, ← ψ.TypeVar_open_Monotype_open_comm τlc <| Nat.zero_ne_add_one _, ← QualifiedType.Monotype_open, ← Monotype_open] exact this all_goals nomatch σke all_goals nomatch σke all_goals nomatch σke | .ind ρ => rw [Monotype.TypeVar_open] at σke generalize A'eq : A.TypeVar_open a n = A' at σke let .ind I₀ I₁ ρke κe keBₗ keBᵣ (κ := κ) := σke rcases Type.ind_evidence_inversion A'eq with ⟨Bₗ', Bᵣ', A'', rfl, rfl, rfl, rfl⟩ rw [Monotype.Monotype_open] simp [Type.Type_open] rw [← QualifiedType.TypeVar_open, ← TypeVar_open] at ρke rw [Monotype.freeTypeVars] at aninσ simp [Type.freeTypeVars] at aninA let ⟨aninBₗ', aninBᵣ', aninA''⟩ := aninA let ρke' := ρke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' aninσ aninA'' τke apply «ind» (I₀ ++ [[(Γ, a : κ₀, Γ')]].typeVarDom) (I₁ ++ [[(Γ, a : κ₀, Γ')]].typeVarDom) ρke' κe · intro aₗ aₗnin aₜ aₜnin aₚ aₚnin aᵢ aᵢnin let ⟨aₗninI₀, aₗninΓaΓ'⟩ := List.not_mem_append'.mp aₗnin let ⟨aₜneaₗ, aₜnin'⟩ := List.not_mem_cons.mp aₜnin let ⟨aₜninI₀, aₜninΓaΓ'⟩ := List.not_mem_append'.mp aₜnin' let aₜninI₀' := List.not_mem_cons.mpr ⟨aₜneaₗ, aₜninI₀⟩ let aₜninΓaΓ'' := List.not_mem_cons.mpr ⟨aₜneaₗ, aₜninΓaΓ'⟩ let ⟨aₚneaₜ, aₚnin'⟩ := List.not_mem_cons.mp aₚnin let ⟨aₚneaₗ, aₚnin''⟩ := List.not_mem_cons.mp aₚnin' let ⟨aₚninI₀, aₚninΓaΓ'⟩ := List.not_mem_append'.mp aₚnin'' let aₚninI₀' := List.not_mem_cons.mpr ⟨aₚneaₜ, List.not_mem_cons.mpr ⟨aₚneaₗ, aₚninI₀⟩⟩ let aₚninΓaΓ'' := List.not_mem_cons.mpr ⟨aₚneaₜ, List.not_mem_cons.mpr ⟨aₚneaₗ, aₚninΓaΓ'⟩⟩ let ⟨aᵢneaₚ, aᵢnin'⟩ := List.not_mem_cons.mp aᵢnin let ⟨aᵢneaₜ, aᵢnin''⟩ := List.not_mem_cons.mp aᵢnin' let ⟨aᵢneaₗ, aᵢnin'''⟩ := List.not_mem_cons.mp aᵢnin'' let ⟨aᵢninI₀, aᵢninΓaΓ'⟩ := List.not_mem_append'.mp aᵢnin''' let aᵢninI₀' := List.not_mem_cons.mpr ⟨aᵢneaₚ, List.not_mem_cons.mpr ⟨aᵢneaₜ, List.not_mem_cons.mpr ⟨aᵢneaₗ, aᵢninI₀⟩⟩⟩ let aᵢninΓaΓ'' := List.not_mem_cons.mpr ⟨aᵢneaₚ, List.not_mem_cons.mpr ⟨aᵢneaₜ, List.not_mem_cons.mpr ⟨aᵢneaₗ, aᵢninΓaΓ'⟩⟩⟩ let keBₗ' : KindingAndElaboration Γc [[(Γ, a : κ₀, Γ', aₗ : L, aₜ : κ, aₚ : R κ, aᵢ : R κ)]] ((qual (.mono (.concat (.var aₚ) (.comm .non) (.row [(.var aₗ, .var aₜ)] none) (.var aᵢ)))).TypeVar_open a (n + 6)) .constr (((((Bₗ'.TypeVar_open aₗ 4).TypeVar_open aₜ 3).TypeVar_open aₚ 2).TypeVar_open aᵢ 1).TypeVar_open a (n + 6)) := by rw [TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, Monotype.TypeVar_open, if_neg nofun, Monotype.TypeVar_open, if_neg nofun, Monotype.TypeVar_open, Monotype.TypeVar_open, List.mapMem_eq_map, List.map_singleton, Monotype.TypeVar_open, if_neg nofun, Monotype.TypeVar_open, if_neg nofun, Type.TypeVar_open_comm (m := 1) (n := n + 6) _ (by simp_arith), Type.TypeVar_open_comm (m := 2) (n := n + 6) _ (by simp_arith), Type.TypeVar_open_comm (m := 3) (n := n + 6) _ (by simp_arith), Type.TypeVar_open_comm (m := 4) (n := n + 6) _ (by simp_arith)] exact keBₗ _ aₗninI₀ _ aₜninI₀' _ aₚninI₀' _ aᵢninI₀' let aneaₗ : a ≠ aₗ := by rw [TypeEnvironment.typeVarDom_append] at aₗninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aₗninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aneaₚ : a ≠ aₚ := by rw [TypeEnvironment.typeVarDom_append] at aₚninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aₚninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aneaₜ : a ≠ aₜ := by rw [TypeEnvironment.typeVarDom_append] at aₜninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aₜninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aneaᵢ : a ≠ aᵢ := by rw [TypeEnvironment.typeVarDom_append] at aᵢninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aᵢninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aninΓ'aₗaₜaₚaᵢaₙ := List.not_mem_cons.mpr ⟨ aneaᵢ, List.not_mem_cons.mpr ⟨aneaₚ, List.not_mem_cons.mpr ⟨aneaₜ, List.not_mem_cons.mpr ⟨aneaₗ, aninΓ'⟩⟩⟩ ⟩ let keBₗ'' := keBₗ'.Monotype_open_preservation Γcw (ΓaΓ'we.typeExt aₗninΓaΓ' .label |>.typeExt aₜninΓaΓ'' κe |>.typeExt aₚninΓaΓ'' κe.row |>.typeExt aᵢninΓaΓ'' κe.row) aninΓ'aₗaₜaₚaᵢaₙ (by simp [freeTypeVars, QualifiedType.freeTypeVars, Monotype.freeTypeVars] exact ⟨aneaₚ, aneaₗ, aneaₜ, aneaᵢ⟩) (Type.not_mem_freeTypeVars_TypeVar_open_intro (Type.not_mem_freeTypeVars_TypeVar_open_intro (Type.not_mem_freeTypeVars_TypeVar_open_intro (Type.not_mem_freeTypeVars_TypeVar_open_intro aninBₗ' aneaₗ) aneaₜ) aneaₚ) aneaᵢ) τke let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [TypeEnvironment.TypeVar_subst, TypeEnvironment.TypeVar_subst, TypeEnvironment.TypeVar_subst, TypeEnvironment.TypeVar_subst, ← Blc.weaken (n := 1).Type_open_TypeVar_open_comm (by simp_arith), ← Blc.weaken (n := 2).Type_open_TypeVar_open_comm (by simp_arith), ← Blc.weaken (n := 3).Type_open_TypeVar_open_comm (by simp_arith), ← Blc.weaken (n := 4).Type_open_TypeVar_open_comm (by simp_arith), Monotype_open, QualifiedType.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open, if_neg nofun, Monotype.Monotype_open, if_neg nofun, Monotype.Monotype_open, Monotype.Monotype_open, List.mapMem_eq_map, List.map_singleton, Monotype.Monotype_open, if_neg nofun, Monotype.Monotype_open, if_neg nofun] at keBₗ'' exact keBₗ'' · intro aᵢ aᵢnin aₙ aₙnin let ⟨aᵢninI₁, aᵢninΓaΓ'⟩ := List.not_mem_append'.mp aᵢnin let ⟨aₙneaᵢ, aₙnin'⟩ := List.not_mem_cons.mp aₙnin let ⟨aₙninI₁, aₙninΓaΓ'⟩ := List.not_mem_append'.mp aₙnin' let aₙninI₁' := List.not_mem_cons.mpr ⟨aₙneaᵢ, aₙninI₁⟩ let aₙninΓaΓ'' := List.not_mem_cons.mpr ⟨aₙneaᵢ, aₙninΓaΓ'⟩ let keBᵣ' : KindingAndElaboration Γc [[(Γ, a : κ₀, Γ', aᵢ : R κ, aₙ : R κ)]] ((qual (.mono (.concat (.var aᵢ) (.comm .non) (.var aₙ) ρ))).TypeVar_open a m) .constr (((Bᵣ'.TypeVar_open aᵢ 1).TypeVar_open aₙ).TypeVar_open a (n + 6)) := by rw [TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, Monotype.TypeVar_open, if_neg nofun, Monotype.TypeVar_open, if_neg nofun, Monotype.TypeVar_open, Type.TypeVar_open_comm (m := 0) (n := n + 6) _ (Nat.zero_ne_add_one _), Type.TypeVar_open_comm (m := 1) (n := n + 6) _ (by simp_arith)] exact keBᵣ _ aᵢninI₁ _ aₙninI₁' let aneaᵢ : a ≠ aᵢ := by rw [TypeEnvironment.typeVarDom_append] at aᵢninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aᵢninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aneaₙ : a ≠ aₙ := by rw [TypeEnvironment.typeVarDom_append] at aₙninΓaΓ' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aₙninΓaΓ' symm exact List.ne_of_not_mem_cons aninΓa let aninΓ'aᵢaₙ := List.not_mem_cons.mpr ⟨aneaₙ, List.not_mem_cons.mpr ⟨aneaᵢ, aninΓ'⟩⟩ let keBᵣ'' := keBᵣ'.Monotype_open_preservation Γcw (ΓaΓ'we.typeExt aᵢninΓaΓ' κe.row |>.typeExt aₙninΓaΓ'' κe.row) aninΓ'aᵢaₙ (by simp [freeTypeVars, QualifiedType.freeTypeVars, Monotype.freeTypeVars] exact ⟨aneaᵢ, aneaₙ, aninσ⟩) (Type.not_mem_freeTypeVars_TypeVar_open_intro (Type.not_mem_freeTypeVars_TypeVar_open_intro aninBᵣ' aneaᵢ) aneaₙ) τke let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [TypeEnvironment.TypeVar_subst, TypeEnvironment.TypeVar_subst, ← Blc.Type_open_TypeVar_open_comm (Nat.succ_ne_zero _), ← Blc.weaken (n := 1).Type_open_TypeVar_open_comm (by simp_arith), Monotype_open, QualifiedType.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open] at keBᵣ'' exact keBᵣ'' | .split (.mk κ τ'') ρ₀ ρ₁ ρ₂ => rw [Monotype.TypeVar_open, TypeLambda.TypeVar_open] at σke let .split concatke := σke rw [Monotype.Monotype_open, TypeLambda.Monotype_open] let concatke' : KindingAndElaboration _ _ (TypeVar_open (.qual (.mono (.concat (.lift (.mk _ τ'') ρ₀) (.comm .comm) ρ₁ ρ₂))) a m) .. := by rw [TypeVar_open, QualifiedType.TypeVar_open, Monotype.TypeVar_open, Monotype.TypeVar_open, Monotype.TypeVar_open, TypeLambda.TypeVar_open] exact concatke rw [Monotype.freeTypeVars] at aninσ let concatke'' := concatke'.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (by rw [freeTypeVars, QualifiedType.freeTypeVars, Monotype.freeTypeVars, Monotype.freeTypeVars, Monotype.freeTypeVars, List.append_nil] exact aninσ ) aninA τke rw [Monotype_open, QualifiedType.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open, Monotype.Monotype_open, TypeLambda.Monotype_open] at concatke'' exact split concatke'' | .qual ψ γ' => rw [QualifiedType.TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case arr => let .qual ψke γ'ke := σke rw [QualifiedType.Monotype_open, Type.Type_open] rw [← QualifiedType.TypeVar_open] at ψke rw [← TypeVar_open] at ψke γ'ke rw [Type.freeTypeVars] at aninA let ψke' := ψke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_left _ ·) (aninA <| List.mem_append_left _ ·) τke let γ'ke' := γ'ke.Monotype_open_preservation Γcw ΓaΓ'we aninΓ' (aninσ <| List.mem_append_right _ ·) (aninA <| List.mem_append_right _ ·) τke rw [Monotype_open] at ψke' γ'ke' rw [QualifiedType.Monotype_open] at ψke' exact qual ψke' γ'ke' all_goals nomatch σke | .quant κ σ' => rw [TypeVar_open] at σke cases A <;> rw [Type.TypeVar_open] at σke case var => split at σke <;> nomatch σke case «forall» K A => let .scheme I σ'ke κe := σke rw [Monotype_open, Type.Type_open] apply scheme ([[(Γ, a : κ₀, Γ')]].typeVarDom ++ I) _ κe intro a' a'nin let ⟨a'ninΓaΓ'', a'ninI⟩ := List.not_mem_append'.mp a'nin have a'ninΓa : [[a' ∉ dom(Γ, a : κ₀)]] := by rw [TypeEnvironment.typeVarDom_append] at a'ninΓaΓ'' exact List.not_mem_append'.mp a'ninΓaΓ'' |>.right let ne := List.ne_of_not_mem_cons a'ninΓa symm at ne let ⟨_, .typeExt Γwe ..⟩ := ΓaΓ'we.append_left_elim let ⟨_, κ₀e⟩ := κ₀.Elaboration_total let Blc := τke.soundness Γcw Γwe κ₀e |>.TypeVarLocallyClosed_of rw [Blc.Type_open_TypeVar_open_comm <| Nat.succ_ne_zero _] have := σ'ke a' a'ninI rw [σ'.TypeVar_open_comm <| Nat.succ_ne_zero _, A.TypeVar_open_comm <| Nat.succ_ne_zero _, ← TypeEnvironment.append] at this rw [freeTypeVars] at aninσ rw [Type.freeTypeVars] at aninA have := this.Monotype_open_preservation Γcw (ΓaΓ'we.typeExt a'ninΓaΓ'' κe) (List.not_mem_cons.mpr ⟨ne, aninΓ'⟩) (not_mem_freeTypeVars_TypeVar_open_intro aninσ ne) (Type.not_mem_freeTypeVars_TypeVar_open_intro aninA ne) τke rw [← TypeEnvironment.append, ← TypeEnvironment.TypeVar_subst, ← σ'.TypeVar_open_Monotype_open_comm τlc <| Nat.zero_ne_add_one _] exact this all_goals nomatch σke termination_by [[Γ, a : κ₀, Γ']].sizeOf' + σ.sizeOf' decreasing_by all_goals simp_arith; try simp_arith [h, TypeEnvironment.append, TypeEnvironment.sizeOf'] · simp_arith [TypeEnvironment.sizeOf'_append, TypeEnvironment.sizeOf'] · rw [← List.getD_eq_getElem?_getD, ← List.get!_eq_getD] apply Nat.le_add_right_of_le apply Nat.le_add_right_of_le apply List.le_sum_of_mem' apply List.mem_map.mpr exact ⟨_, List.get!_mem ilt, rfl⟩ · rw [← List.getD_eq_getElem?_getD, ← List.get!_eq_getD] apply Nat.le_add_right_of_le apply Nat.le_trans _ <| Nat.le_add_left _ _ apply List.le_sum_of_mem' apply List.mem_map.mpr exact ⟨_, List.get!_mem ilt, rfl⟩ · exact Nat.succ_le_of_lt <| Monotype.sizeOf'_pos _ · exact Nat.succ_le_of_lt <| Monotype.sizeOf'_pos _ · exact Nat.succ_le_of_lt <| QualifiedType.sizeOf'_pos _ · simp_arith [TypeEnvironment.sizeOf'_append, TypeEnvironment.sizeOf'] theorem TypeEnvironment.WellFormednessAndElaboration.TypeVar_subst_preservation (ΓaΓ'we : [[Γc ⊢ Γ, a : κ, Γ' ⇝ Δ, a : K, Δ']]) (Γcw : [[⊢c Γc]]) (aninΓ' : [[a ∉ dom(Γ')]]) (τke : [[Γc; Γ ⊢ τ : κ ⇝ B]]) : [[Γc ⊢ Γ, Γ' [τ / a] ⇝ Δ, Δ' [B / a] ]] := by match Γ' with | .empty => match Δ' with | .empty => let .typeExt Γwe .. := ΓaΓ'we exact Γwe | .typeExt .. => let .typeExt Γwe aninΓ _ := ΓaΓ'we let aninΔaΔ'' := Γwe.TypeVarNotInDom_preservation aninΓ rw [Environment.TypeVarNotInDom, Environment.TypeVarInDom, Environment.typeVarDom_append] at aninΔaΔ'' let ⟨_, aninΔa⟩ := List.not_mem_append'.mp aninΔaΔ'' nomatch aninΔa <| .head _ | .typeExt .. => match Δ' with | .empty => let .typeExt _ aninΓaΓ'' _ := ΓaΓ'we rw [TypeEnvironment.TypeVarNotInDom, TypeEnvironment.typeVarDom_append] at aninΓaΓ'' let ⟨_, aninΓa⟩ := List.not_mem_append'.mp aninΓaΓ'' nomatch aninΓa <| .head _ | .typeExt .. => let .typeExt ΓaΓ''we a'ninΓaΓ'' κ'e := ΓaΓ'we rw [TypeEnvironment.TypeVar_subst, Environment.TypeVar_subst, TypeEnvironment.append, Environment.append] rw [TypeEnvironment.TypeVarNotInDom] at aninΓ' let aninΓ'' := List.not_mem_of_not_mem_cons aninΓ' rw [TypeEnvironment.TypeVarNotInDom, TypeEnvironment.typeVarDom_append] at a'ninΓaΓ'' let ⟨a'ninΓ'', a'ninΓa⟩ := List.not_mem_append'.mp a'ninΓaΓ'' let a'ninΓ := List.not_mem_of_not_mem_cons a'ninΓa rw [← TypeEnvironment.TypeVarNotInDom] at a'ninΓ'' let a'ninΓ'' := a'ninΓ''.TypeVar_subst_preservation (a' := a) (τ := τ) let a'ninΓΓ'' := List.not_mem_append'.mpr ⟨a'ninΓ'', a'ninΓ⟩ rw [← TypeEnvironment.typeVarDom_append] at a'ninΓΓ'' exact ΓaΓ''we.TypeVar_subst_preservation Γcw aninΓ'' τke |>.typeExt a'ninΓΓ'' κ'e | .termExt .. => let .termExt .. := Δ' let .termExt ΓaΓ''we xninΓaΓ'' σke := ΓaΓ'we rw [TypeEnvironment.TypeVar_subst, Environment.TypeVar_subst, TypeEnvironment.append, Environment.append] rw [TypeEnvironment.TermVarNotInDom, TypeEnvironment.termVarDom_append] at xninΓaΓ'' let ⟨xninΓ'', xninΓa⟩ := List.not_mem_append'.mp xninΓaΓ'' rw [← TypeEnvironment.TermVarNotInDom] at xninΓ'' let xninΓ'' := xninΓ''.TypeVar_subst_preservation (a := a) (τ := τ) rw [TypeEnvironment.termVarDom] at xninΓa let xninΓΓ'' := List.not_mem_append'.mpr ⟨xninΓ'', xninΓa⟩ rw [← TypeEnvironment.termVarDom_append] at xninΓΓ'' apply ΓaΓ''we.TypeVar_subst_preservation Γcw aninΓ' τke |>.termExt xninΓΓ'' _ let σlc := σke.TypeVarLocallyClosed_of let Blc := σke.soundness Γcw ΓaΓ''we .star |>.TypeVarLocallyClosed_of rw [← σlc.TypeVar_open_TypeVar_close_id (a := a), ← Blc.TypeVar_open_TypeVar_close_id (a := a)] at σke have := σke.Monotype_open_preservation Γcw ΓaΓ''we aninΓ' not_mem_freeTypeVars_TypeVar_close Type.not_mem_freeTypeVars_TypeVar_close τke rw [σlc.Monotype_open_TypeVar_close_eq_TypeVar_subst, Blc.Type_open_TypeVar_close_eq_TypeVar_subst] at this exact this | .constrExt .. => let .termExt .. := Δ' let .constrExt ΓaΓ''we xninΓaΓ'' ψke := ΓaΓ'we rw [TypeEnvironment.TypeVar_subst, Environment.TypeVar_subst, TypeEnvironment.append, Environment.append] rw [TypeEnvironment.TermVarNotInDom, TypeEnvironment.termVarDom_append] at xninΓaΓ'' let ⟨xninΓ'', xninΓa⟩ := List.not_mem_append'.mp xninΓaΓ'' rw [← TypeEnvironment.TermVarNotInDom] at xninΓ'' let xninΓ'' := xninΓ''.TypeVar_subst_preservation (a := a) (τ := τ) rw [TypeEnvironment.termVarDom] at xninΓa let xninΓΓ'' := List.not_mem_append'.mpr ⟨xninΓ'', xninΓa⟩ rw [← TypeEnvironment.termVarDom_append] at xninΓΓ'' apply ΓaΓ''we.TypeVar_subst_preservation Γcw aninΓ' τke |>.constrExt xninΓΓ'' _ let ψlc := ψke.TypeVarLocallyClosed_of let Blc := ψke.soundness Γcw ΓaΓ''we .constr |>.TypeVarLocallyClosed_of rw [← ψlc.TypeVar_open_TypeVar_close_id (a := a), ← Blc.TypeVar_open_TypeVar_close_id (a := a)] at ψke have := ψke.Monotype_open_preservation Γcw ΓaΓ''we aninΓ' not_mem_freeTypeVars_TypeVar_close Type.not_mem_freeTypeVars_TypeVar_close τke rw [ψlc.Monotype_open_TypeVar_close_eq_TypeVar_subst, Blc.Type_open_TypeVar_close_eq_TypeVar_subst] at this exact this termination_by [[Γ, a : κ, Γ']].sizeOf' decreasing_by all_goals simp_arith [TypeEnvironment.append, TypeEnvironment.sizeOf'] end end TabularTypes