Proofgold Proposition

∀ x0 . nat_p x0 ⟶ setsum 1 x0 = ordsucc x0

type
prop

theory
HF

name
-

proof
PUaiy..

Megalodon
nat_pair1_ordsucc

proofgold address
TMQ5j..^{nat_pair1_ordsucc}

creator
1504 PrGxv../9d1f0..

owner
1504 PrGxv../9d1f0..

term root
14a19..