induction p using Formula.rec' with
| hatom => apply M.hereditary hw;
| himp =>
  simp_all [Satisfies];
  intro hpq v hv;
  exact hpq $ M.Frame.Rel_trans hw hv;
| hor => simp_all [Satisfies]; tauto;
| _ => simp_all [Satisfies];
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
p : Formula α
hw : w ≺ w'
⊢ Satisfies M w p → Satisfies M w' p
no goals