conv =>
  lhs
  simp only [Var.freeVarSet]
z : String
t : Var
i : ℕ
⊢ (bound_ i).freeVarSet ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}
z : String
t : Var
i : ℕ
⊢ ∅ ⊆ t.freeVarSet ∪ (bound_ i).freeVarSet \ {free_ z}