cases v
v : Var
σ : String → String
j : ℕ
z : String
h1 : σ z = z
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) v) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) v)
case free_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ a✝))

case bound_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ a✝))