induction d with
| eaxm h => exact validOnAxiomSetFrameClass_axiom h hF;
| mdp _ _ ihpq ihp => exact ValidOnFrame.mdp ihpq ihp;
| _ =>
  intros;
  first
  | apply ValidOnFrame.verum
  | apply ValidOnFrame.imply₁
  | apply ValidOnFrame.imply₂
  | apply ValidOnFrame.disj₁
  | apply ValidOnFrame.disj₂
  | apply ValidOnFrame.disj₃
  | apply ValidOnFrame.conj₁
  | apply ValidOnFrame.conj₂
  | apply ValidOnFrame.conj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
d : 𝓓 ⊢ p
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
⊢ F ⊧ p
no goals