existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ x,
    ∃ (x_1 : ∀ {w₁ w₂ : LEMCounterexampleModel.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ¬ValidOnModel { Frame := LEMCounterexampleModel.Frame, Valuation := x, hereditary := x_1 }
          (atom default ⋎ (atom default ⟶ ⊥))
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))