apply intro_union_ParametricConsistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ (L)-Consistent (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {Γ₁ Γ₂ : List (Formula α)},
    (∀ p ∈ Γ₁, p ∈ □''⁻¹Ω₁.theory) → (∀ p ∈ Γ₂, p ∈ ◇''^[n]Ω₂.theory) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥