Proofgold Proposition

∀ x0 : ι → ι . ∀ x1 . nat_p x1 ⟶ finite_add_SNo (ordsucc x1) x0 = add_SNo (finite_add_SNo x1 x0) (x0 x1)

type
prop

theory
HotG

name
-

proof
PULfh..

Megalodon
-

proofgold address
TMa16..

creator
16612 PrGxv../8d33a..

owner
16612 PrGxv../8d33a..

term root
69fae..