Proofgold Proposition

∀ x0 x1 : ι → ι → ο . wceq (cmpt x0 x1) (copab (λ x2 x3 . wa (wcel (cv x2) (x0 x2)) (wceq (cv x3) (x1 x2))))

type
prop

theory
SetMM

name
df_mpt

proof
PUQyb..

Megalodon
-

proofgold address
TMc3n..

creator
36397 PrCmT../edba3..

owner
36397 PrCmT../edba3..

term root
52df4..