. intro h Ω;
  suffices p ∈ Ω.theory by exact truthlemma.mpr this;
  by_contra hC;
  have := MaximalParametricConsistentTheory.maximal' hC;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Theory.iff_insert_notParametricConsistent.mp this;
  exact Ω.consistent hΓ₁ $ andImplyIffImplyImply'!.mp hΓ₂ ⨀ h;
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ L ⊢! p → CanonicalModel L ⊧ p
no goals