try simp_all
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹)) -
      node_to_multiset (Lnew, Rnew, none)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)) ++ [~unload val✝¹.1])
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹)) -
      node_to_multiset (Lnew, Rnew, none)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ (Rnew ++ [~unload val✝¹.1]))))