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
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd :: tl).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (hd :: tl)).toFinset.biUnion Var.freeVarSet
no goals