Proofgold Proposition

∀ x0 . nat_p x0 ⟶ prim3 (ordsucc x0) = x0

type
prop

theory
HotG

name
Union_ordsucc_eq

proof
PUL8Q..

Megalodon
Union_ordsucc_eq

proofgold address
TMWEc..^{Union_ordsucc_eq}

creator
4882 Pr6Pc../b0bd0..

owner
4882 Pr6Pc../b0bd0..

term root
87308..