Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_ordinal_ordinal__4__2

proofgold address
TMXMH..^{Conj_add_SNo_ordinal_ordinal__4__2}

creator
35053 PrNpY../7edb1..

owner
35061 PrNpY../65f52..

term root
ad88d..