subst def_f
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
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
g : Formula
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g
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
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : evaluate M w (Con (X ++ (Option.map negUnload none).toList))
⊢ g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr (~'χ)))).toList → evaluate M w g