Proofgold Proposition

wceq cfin2 (cab (λ x0 . wral (λ x1 . wa (wne (cv x1) c0) (wor (cv x1) crpss) ⟶ wcel (cuni (cv x1)) (cv x1)) (λ x1 . cpw (cpw (cv x0)))))

type
prop

theory
SetMM

name
df_fin2

proof
PUhHD..

Megalodon
-

proofgold address
TMRNc..

creator
36397 PrCmT../a4681..

owner
36397 PrCmT../a4681..

term root
58d65..