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})
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
case s1
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} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}

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
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (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