. simp [ValidOnFrame];
  existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary;
  apply noLEM_atom;
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
no goals