Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2 ∈ prim5 x0 x1) (∃ x3 . and (x3 ∈ x0) (x2 = x1 x3))

as obj
-

as prop
47112..^ReplEq

theory
HotG

stx
cde1e..

address
TMHvG..^ReplEq