Proofgold Term Root Disambiguation

∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2

as obj
-

as prop
66f4d..^{ordsucc_inj_contra}

theory
HotG

stx
019b2..

address
TMa7r..^{ordsucc_inj_contra}