cases Ω₂
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✝ } = Ω₂
case mpr.mk.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
theory✝ : Theory α
consistent✝ : (L)-Consistent theory✝
maximal✝ : ∀ {U : Theory α}, theory✝ ⊂ U → ¬(L)-Consistent U
h :
  { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ }.theory =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }.theory
⊢ { theory := theory✝¹, consistent := consistent✝¹, maximal := maximal✝¹ } =
    { theory := theory✝, consistent := consistent✝, maximal := maximal✝ }