case free_ x =>
  simp only [Var.subst]
  split_ifs
  case pos c1 =>
    apply Finset.subset_union_left
  case neg c1 =>
    have s1 : Var.freeVarSet (free_ x) \ {free_ z} = {free_ x}
    simp only [Var.freeVarSet]
    simp
    simp at c1
    exact c1
    simp only [s1]
    apply Finset.subset_union_right
z : String
t : Var
x : String
⊢ ((free_ z).subst t (free_ x)).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
no goals