use (L ++ X, R, some (Sum.inl val))
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
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
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
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl val))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl val))