Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SNo x0 ⟶ SNo (add_SNo x0 x1) ⟶ ordinal (add_SNo x0 x1)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_ordinal_ordinal__3__3

proofgold address
TMaFB..^{Conj_add_SNo_ordinal_ordinal__3__3}

creator
35053 PrNpY../4e7e0..

owner
35062 PrNpY../3faac..

term root
b4fe2..