Proofgold Proposition

∀ x0 x1 . not (x0 = x1) ⟶ not (ordsucc x0 = ordsucc x1)

type
prop

theory
HF

name
-

proof
PUTdW..

Megalodon
ordsucc_inj_contra

proofgold address
TMacQ..^{ordsucc_inj_contra}

creator
1473 PrGxv../2662d..

owner
1473 PrGxv../2662d..

term root
0ce6d..