Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (prim1 x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (prim1 x1 x0 ⟶ x2) ⟶ x2

type
prop

theory
HoTg

name
ordinal_trichotomy_or_impred

proof
PUbD9..

Megalodon
-

proofgold address
TMSqR..

creator
4079 PrGxv../a2a1c..

owner
4079 PrGxv../a2a1c..

term root
7c0f0..