Proofgold Proposition

∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)

type
prop

theory
HF

name
-

proof
PUVGM..

Megalodon
add_nat_SR

proofgold address
TMQDX..^add_nat_SR

creator
2277 PrGxv../9fb87..

owner
2277 PrGxv../9fb87..

term root
bfc87..