Proofgold Term Root Disambiguation

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

as obj
13545..^atleastp

as prop
-

theory
HotG

stx
18c18..

address
TMdn3..^atleastp