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