case LRnegR φ hC =>
  subst hC
  simp [applyLocalRule] at *
  intro hyp
  have := hyp φ
  have := hyp (~φ)
  aesop
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.LRnegR φ) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
no goals