Proofgold Term Root Disambiguation

λ x0 . λ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)

as obj
0bcfd..

as prop
-

theory
HoTg

stx
7f654..

address
TMWJ8..^PNoEq_