split_ifs
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝ : 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))

case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

case neg
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬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))