simp [applyLocalRule] at *
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegR φ) (L, R, O), (M, w)⊨Ci
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)