Proofgold Proposition

wceq crngo (copab (λ x0 x1 . wa (wa (wcel (cv x0) cablo) (wf (cxp (crn (cv x0)) (crn (cv x0))) (crn (cv x0)) (cv x1))) (wa (wral (λ x2 . wral (λ x3 . wral (λ x4 . w3a (wceq (co (co (cv x2) (cv x3) (cv x1)) (cv x4) (cv x1)) (co (cv x2) (co (cv x3) (cv x4) (cv x1)) (cv x1))) (wceq (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x1)) (co (co (cv x2) (cv x3) (cv x1)) (co (cv x2) (cv x4) (cv x1)) (cv x0))) (wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x1)) (co (co (cv x2) (cv x4) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0)))) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0))) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0))))))

type
prop

theory
SetMM

name
df_rngo

proof
PUMry..

Megalodon
-

proofgold address
TMJ3u..

creator
36377 PrCmT../adc44..

owner
36377 PrCmT../adc44..

term root
5c00b..