simp only [List.mem_union_iff, List.mem_append, List.mem_singleton] at g_in
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
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ∪ (R ++ X) ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ 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
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : (g ∈ L ∨ g ∈ R ∨ g ∈ X) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inr val))).toList
⊢ evaluate M w g