simp only [Var.substFun]
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    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
c2 : ¬i = j
⊢ bound_ (i - 1) = Var.open j (free_ z) (bound_ i)