Proofgold Proposition

∀ x0 x1 : ι → ο . wceq (bj_c2uple x0 x1) (cun (bj_c1upl x0) (cxp (csn c1o) (bj_ctag x1)))

type
prop

theory
SetMM

name
df_bj_2upl

proof
PUMPg..

Megalodon
-

proofgold address
TMH9Y..

creator
36399 PrCmT../4d6a5..

owner
36399 PrCmT../4d6a5..

term root
ff254..