simp [ihc, ihg]
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 (0 + 1)
    ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
      Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
no goals