exact h (by
  apply iff_definability_memAxiomSetFrameClass instClassicalDefinabilityExtensive |>.mpr;
  simp [Extensive];
) (ClassicalModel V).Valuation (ClassicalModel V).hereditary
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p
no goals