constructor
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ ↔ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂