simp only [Formula.freeVarSet]
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X (List.map ((free_ z).subst t) vs)).freeVarSet ⊆ t.freeVarSet ∪ (pred_ X vs).freeVarSet \ {free_ z}
z : String
t : Var
X : String
vs : List Var
⊢ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet ⊆
    t.freeVarSet ∪ vs.toFinset.biUnion Var.freeVarSet \ {free_ z}