try apply List.Sublist.subperm
case h.refine_2.refine_1.h.some.inr.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝²)) ∈ 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✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²))
⊢ (Lnew ++ Rnew).Subperm (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))
case h.refine_2.refine_1.h.some.inr.some.inr.some.inr.s
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝²)) ∈ 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✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²))
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))