case free_ x =>
  simp only [Var.subst]
  split_ifs
  case pos c1 =>
    simp only [c1]
    conv =>
      lhs
      simp only [Var.freeVarSet]
    simp
  case neg c1 =>
    simp only [Var.freeVarSet]
    exact Finset.sdiff_subset {free_ x} {free_ z}
z : String
t : Var
x : String
⊢ (free_ x).freeVarSet \ {free_ z} ⊆ ((free_ z).subst t (free_ x)).freeVarSet
no goals