have : evaluate M w (discon ress) := by
  rw [← osTruth, conEval]
  intro f f_in; apply w_LRO
  simp only [List.mem_union_iff, List.mem_append]
  exact Or.inl $ Or.inr $ List.Sublist.subset preconditionProof f_in
case mp
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)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
case mp
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)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)