Proofgold Proposition

∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ ordsucc x0 = ordsucc x1 ⟶ ∀ x2 : ο . x2

type
prop

theory
HotG

name
ordsucc_inj_contra

proof
PUUcH..

Megalodon
ordsucc_inj_contra

proofgold address
TMKVL..^{ordsucc_inj_contra}

creator
4892 Pr6Pc../65c97..

owner
4892 Pr6Pc../65c97..

term root
79130..