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