induction vs
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
case nil
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet

case cons
z : String
t : Var
X : String
head✝ : Var
tail✝ : List Var
tail_ih✝ :
  tail✝.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) tail✝).toFinset.biUnion Var.freeVarSet
⊢ (head✝ :: tail✝).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (head✝ :: tail✝)).toFinset.biUnion Var.freeVarSet