Proofgold Proposition

wceq cmp (cmpt2 (λ x0 x1 . cnp) (λ x0 x1 . cnp) (λ x0 x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (co (cv x3) (cv x4) cmq)) (λ x4 . cv x1)) (λ x3 . cv x0))))

type
prop

theory
SetMM

name
df_mp

proof
PUc2k..

Megalodon
-

proofgold address
TMMqL..

creator
36396 PrCmT../c13e0..

owner
36396 PrCmT../c13e0..

term root
045d2..