constructor
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)

case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))