cases Ω₁
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
h : Ω₁.theory = Ω₂.theory
⊢ Ω₁ = Ω₂
case mpr.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₂ : MCT L
p : Formula α
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h : { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory = Ω₂.theory
⊢ { theory := theory✝, consistent := consistent✝, maximal := maximal✝ } = Ω₂