Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cdpj (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cima (cdm cdprd) (csn (cv x0))) (λ x0 x1 . cmpt (λ x2 . cdm (cv x1)) (λ x2 . co (cfv (cv x2) (cv x1)) (co (cv x0) (cres (cv x1) (cdif (cdm (cv x1)) (csn (cv x2)))) cdprd) (cfv (cv x0) cpj1))))
as obj
-
as prop
1bff7..
theory
SetMM
stx
9edd3..
address
TMJsW..