induction d using Deduction.inducition_with_nec with
| hMaxm h => exact validOnAxiomSetFrameClass_axiom h;
| hMdp _ _ ihpq ihp =>
  intro F hF V w;
  exact Satisfies.mdp (ihpq F hF V w) (ihp F hF V w);
| hNec _ ih =>
  intro F hF V w w' _;
  exact ih F hF V w';
| hDisj₃ =>
  simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
  intros; rename_i hpr hqr hpq;
  cases hpq with
  | inl hp => exact hpr hp;
  | inr hq => exact hqr hq;
| _ => simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel];
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p : Formula α
d : L ⊢ p
⊢ 𝔽(Ax(L)) ⊧ p
no goals