Proofgold Term Root Disambiguation

∀ x0 : ι → ο . x0 1 ⟶ x0 omega ⟶ MetaCat_nno_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) 1 (λ x1 . lam x1 (λ x2 . 0)) omega (lam 1 (λ x1 . 0)) (lam omega ordsucc) (λ x1 x2 x3 . lam omega (nat_primrec (ap x2 0) (λ x4 . ap x3)))

as obj
-

as prop
ea037..^{MetaCatSet_nno_gen}

theory
HotG

stx
c80b6..

address
TMNdg..^{MetaCatSet_nno_gen}