conv =>
  lhs
  simp only [Var.open]
  simp only [Var.substFun]
  simp only [str_fun_to_var_fun]
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ x)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ free_ (σ x) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))