Proofgold Proposition

wceq cfin1a (cab (λ x0 . wral (λ x1 . wo (wcel (cv x1) cfn) (wcel (cdif (cv x0) (cv x1)) cfn)) (λ x1 . cpw (cv x0))))

type
prop

theory
SetMM

name
df_fin1a

proof
PUhHD..

Megalodon
-

proofgold address
TMH64..

creator
36397 PrCmT../cd277..

owner
36397 PrCmT../cd277..

term root
42a90..