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