Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (famunion x0 x1)

as obj
-

as prop
b3f1e..^{ordinal_famunion}

theory
HotG

stx
18c18..

address
TMU1R..^{ordinal_famunion}