Proofgold Proposition

wceq clpir (crab (λ x0 . wceq (cfv (cv x0) clidl) (cfv (cv x0) clpidl)) (λ x0 . crg))

type
prop

theory
SetMM

name
df_lpir

proof
PUN9o..

Megalodon
-

proofgold address
TMYiz..

creator
36376 PrCmT../d3e6d..

owner
36376 PrCmT../d3e6d..

term root
ca83b..