Proofgold Proposition

wceq clpidl (cmpt (λ x0 . crg) (λ x0 . ciun (λ x1 . cfv (cv x0) cbs) (λ x1 . csn (cfv (csn (cv x1)) (cfv (cv x0) crsp)))))

type
prop

theory
SetMM

name
df_lpidl

proof
PUN9o..

Megalodon
-

proofgold address
TMdNe..

creator
36376 PrCmT../ec4a7..

owner
36376 PrCmT../ec4a7..

term root
899bb..