Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι . {x2 ∈ prim4 (lam x0 (λ x2 . prim3 (x1 x2)))|∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3}

as obj
a7b1b..^Pi

as prop
-

theory
HotG

stx
08e38..

address
TMMms..^Pi