Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x1 (Sing 1) ∈ {SetAdjoin x2 (Sing 1)|x2 ∈ x0} ⟶ x1 ∈ x0

as obj
-

as prop
70c25..^tagged_ReplE

theory
HotG

stx
fab7c..

address
TMNf9..^tagged_ReplE