Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . x3 ∈ setexp (setexp x2 x1) x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ap (ap x3 x4) x5 ∈ x2

as obj
-

as prop
69857..

theory
HotG

stx
786b2..

address
TMHEk..