case comp c d ihc ihg =>
  exact Hierarchy.exClosure (by 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 𝚺 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