intro W M w
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
⊢ (~unload χ)≡dis
      (List.map
        (fun x =>
          match x with
          | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
        B)
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          B))