constructor
case h
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, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)) ∧
    evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
case h.left
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, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∃ a b,
    (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)

case h.right
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, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))