rintro ⟨Ci, ⟨⟨X, O, ⟨in_ress, def_Ci⟩⟩, w_Ci⟩⟩
case mpr
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
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
case mpr.intro.intro.intro.intro.intro
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
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inr O with
    | none => (L, R ++ X, some (Sum.inr (~'χ)))
    | some (Sum.inl (~'χ)) => (L, R ++ X, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L, R ++ X, some (Sum.inr (~'χ)))) =
    Ci
⊢ ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f