induction p using Formula.rec' with
| hatom a => simp [Kripke.Satisfies];
| hbox p ih =>
  intro Ω;
  constructor;
  . intro h;
    apply iff_mem_box.mpr;
    intro Ω' hΩ';
    apply ih.mp;
    exact h Ω' hΩ';
  . intro h Ω' hΩ';
    apply ih.mpr;
    exact CanonicalFrame.frame_def_box.mp hΩ' h;
| hfalsum => simp [Formula.Kripke.Satisfies.bot_def (M := (CanonicalModel L))];
| hVerum => simp [Formula.Kripke.Satisfies.top_def (M := (CanonicalModel L))];
| _ => simp_all
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
no goals