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
c1 : ¬free_ z = free_ x
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
no goals