induction c <;> simp[codeAux, Matrix.fun_eq_vec₂]
k : ℕ
c : Code k
⊢ Hierarchy 𝚺 1 (codeAux c)
case comp
k m✝ n✝ : ℕ
a✝¹ : Code n✝
a✝ : Fin n✝ → Code m✝
a_ih✝¹ : Hierarchy 𝚺 1 (codeAux a✝¹)
a_ih✝ : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (a✝ a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))

case rfind
k n✝ : ℕ
a✝ : Code (n✝ + 1)
a_ih✝ : Hierarchy 𝚺 1 (codeAux a✝)
⊢ Hierarchy 𝚺 1 (codeAux a✝) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))))”)