Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (Subq x0 x1) (Subq x1 x0)

type
prop

theory
HF

name
-

proof
PUZ6J..

Megalodon
ordinal_linear

proofgold address
TMLv3..^{ordinal_linear}

creator
1604 PrGxv../5b7b0..

owner
1604 PrGxv../5b7b0..

term root
0f4c8..