Proofgold Proposition

wceq cmpq (cmpt2 (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cop (co (cfv (cv x0) c1st) (cfv (cv x1) c1st) cmi) (co (cfv (cv x0) c2nd) (cfv (cv x1) c2nd) cmi)))

type
prop

theory
SetMM

name
df_mpq

proof
PUc2k..

Megalodon
-

proofgold address
TMHuF..

creator
36396 PrCmT../2affc..

owner
36396 PrCmT../2affc..

term root
0aec9..