Proofgold Term Root Disambiguation

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

as obj
-

as prop
d7246..^{ordinal_famunion}

theory
HF

stx
82de5..

address
TMbgx..^{ordinal_famunion}