exact Or.inl $ Or.inr $ Or.inl $ List.mem_diff_of_mem f_in_R f_notin_cond
case mpr.intro.intro.inl.inr.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
no goals