case bound_ i =>
  conv =>
    lhs
    simp only [Var.open]
  split_ifs
  case pos c1 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_pos c1]
  case pos c1 c2 =>
    simp only [Var.substFun]
    simp only [str_fun_to_var_fun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_pos c2]
    simp only [h1]
  case neg c1 c2 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_neg c2]
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ i)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
no goals