case pos c1 =>
  simp only [Var.substFun]
  simp only [Var.open]
  simp only [if_pos c1]
σ : 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))
no goals