obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Theory.iff_insert_notParametricConsistent.mp this
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
case mpr.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
hC : p ∉ Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ Ω.theory
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False