constructor
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
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
case mp
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
⊢ (M, w)⊨(L, R, O) → ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

case mpr
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
⊢ (∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)) → (M, w)⊨(L, R, O)