have := hyp (~φ)
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)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
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)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False