Theorem: LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.frame_def (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t₁ t₂ : SCT 𝓓
⊢ (CanonicalModel 𝓓).Rel t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1
Tactic:
rfl
State after:
no goals