Proofgold Proposition

∀ x0 x1 x2 : ι → ο . wceq (cwsuc x0 x1 x2) (cinf (cpred x0 (ccnv x1) x2) x0 x1)

type
prop

theory
SetMM

name
df_wsuc

proof
PUcix..

Megalodon
-

proofgold address
TMUGe..

creator
36378 PrCmT../a93d5..

owner
36378 PrCmT../a93d5..

term root
c0903..