Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ prim4 1 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim4 1) ⟶ lam x0 x1 ∈ prim4 1

as obj
-

as prop
889ba..^{Sigma_Power_1}

theory
HotG

stx
08e38..

address
TMTUP..^{Sigma_Power_1}