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