Proofgold Term Root Disambiguation

∀ x0 x1 . Sing 2 ∈ x0 ⟶ ordinal x1 ⟶ not (Sing 2 ∈ SetAdjoin x1 (Sing 1))

as obj
-

as prop
34c67..^{Conj_ctagged_eqE_Subq__1__1}

theory
HotG

stx
b740c..

address
TMbEc..^{Conj_ctagged_eqE_Subq__1__1}