simp only [Var.substFun]
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = Var.open j (free_ z) (bound_ i)