intro h
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.IsNonempty 𝔽ꟳ(Ax(L))
⊢ L ⊬! ⊥
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.IsNonempty 𝔽ꟳ(Ax(L))
h : L ⊢! ⊥
⊢ False