apply noLEM_atom
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))
no goals