Proofgold Proposition

∀ x0 x1 : ι → ι → ο . wceq (ciin x0 x1) (cab (λ x2 . wral (λ x3 . wcel (cv x2) (x1 x3)) x0))

type
prop

theory
SetMM

name
df_iin

proof
PUQyb..

Megalodon
-

proofgold address
TMbyV..

creator
36397 PrCmT../2349c..

owner
36397 PrCmT../2349c..

term root
b64af..