simp [ih]
k✝ k : ℕ
c : Code (k + 1)
ih : Hierarchy 𝚺 1 (codeAux c)
⊢ Hierarchy 𝚺 1 (codeAux c) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))))”)
no goals