simp only [Var.freeVarSet]
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
j : ℕ
z x : String
c1 : ¬free_ x = free_ z
⊢ {free_ x} ⊆ {free_ x} \ {free_ z}