intro hyp
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False