Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 x4 . x3 ∈ ordsucc (ordsucc x0) ⟶ ordsucc x4 ∈ ordsucc (ordsucc x0) ⟶ not (x2 ⊆ x3) ⟶ x2 ⊆ x4 ⟶ x1 x3 = x1 (ordsucc x4) ⟶ x3 = ordsucc x4 ⟶ ∀ x5 : ο . x5

as obj
-

as prop
24d2c..^{Conj_PigeonHole_nat__1__0}

theory
HotG

stx
202df..

address
TMS7s..^{Conj_PigeonHole_nat__1__0}