intro f f_in
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∀ f ∈ Y, evaluate M w f
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f✝ : Formula
f_in_L : f✝ ∈ L
f_in_cond : f✝ ∈ Lcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f