intro f f_in
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.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    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.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    Ci
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
⊢ evaluate M w f