Proofgold Proposition

wceq cdiag (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . co (cop (cv x0) (cv x1)) (co (cv x0) (cv x1) c1stf) ccurf))

type
prop

theory
SetMM

name
df_diag

proof
PUdJh..

Megalodon
-

proofgold address
TMVby..

creator
36384 PrCmT../7bacc..

owner
36384 PrCmT../7bacc..

term root
a6251..