Proofgold Proposition

∀ 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

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_PigeonHole_nat__1__0

proofgold address
TMY6v..^{Conj_PigeonHole_nat__1__0}

creator
35045 PrNpY../8966f..

owner
35047 PrNpY../1aeeb..

term root
d0c8d..