case pred_ X vs =>
  simp only [Formula.subst]
  simp only [Formula.freeVarSet]
  induction vs
  case nil =>
    simp
  case cons hd tl ih =>
    simp
    have s1 : (Var.freeVarSet hd ∪ Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z} = (Var.freeVarSet hd \ {free_ z}) ∪ ((Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z})
    exact Finset.union_sdiff_distrib (Var.freeVarSet hd) (Finset.biUnion (List.toFinset tl) Var.freeVarSet) {free_ z}
    simp only [s1]
    exact Finset.union_subset_union (VarSubstFreeVarSet' z t hd) ih
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X vs).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (pred_ X vs)).freeVarSet
no goals