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