subst hC
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
hC : C = applyLocalRule (LocalRule.LRnegL φ) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
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.LRnegL φ) (L, R, O), (M, w)⊨Ci