simp
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
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.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet