Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . nIn x2 x1 ⟶ nIn x3 x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ atleastp x0 x1 ⟶ atleastp (ordsucc (ordsucc x0)) (binunion x1 (UPair x2 x3))

as obj
-

as prop
0138d..

theory
HotG

stx
0741e..

address
TMdy2..