apply w_LRO f
case h.right.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f
case h.right.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList