conv =>
  lhs
  simp only [Var.freeVarSet]
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ (free_ x).freeVarSet \ {free_ x} ⊆ t.freeVarSet
z : String
t : Var
x : String
c1 : free_ z = free_ x
⊢ {free_ x} \ {free_ x} ⊆ t.freeVarSet