exact Or.inl $ Or.inl $ List.Sublist.subset preconditionProof f_in
case a
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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
no goals