Proofgold Term Root Disambiguation

∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p (λ x4 . x4 ∈ prim6 (prim6 0)) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x0 x2

as obj
-

as prop
b5da2..^{MetaCatSmallSet_terminal}

theory
HotG

stx
2772d..

address
TMZZQ..^{MetaCatSmallSet_terminal}