Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ exactly1of3 (In x0 x1) (x0 = x1) (In x1 x0)

type
prop

theory
HF

name
-

proof
PUZ6J..

Megalodon
ordinal_trichotomy

proofgold address
TMd3y..^{ordinal_trichotomy}

creator
1604 PrGxv../752c0..

owner
1604 PrGxv../752c0..

term root
43f7c..