Proofgold Term Root Disambiguation

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_b_b_e x1) ⟶ MetaCat x0 Hom_b_b_e (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))

as obj
-

as prop
5f5c5..^{MetaCat_struct_b_b_e_gen}

theory
HotG

stx
820be..

address
TMaP4..^{MetaCat_struct_b_b_e_gen}