subst preconditionProof
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
preconditionProof : some (Sum.inr (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, O), (M, w)⊨Ci
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, some (Sum.inr (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, some (Sum.inr (~'χ))), (M, w)⊨Ci