Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 : ι → ι → ο . wceq (citg x0 x1) (csu (co cc0 c3 cfz) (λ x2 . co (co ci (cv x2) cexp) (cfv (cmpt (λ x3 . cr) (λ x3 . csb (cfv (co (x1 x3) (co ci (cv x2) cexp) cdiv) cre) (λ x4 . cif (wa (wcel (cv x3) (x0 x3)) (wbr cc0 (cv x4) cle)) (cv x4) cc0))) citg2) cmul))
type
prop
theory
SetMM
name
df_itg
proof
PUa4n..
Megalodon
-
proofgold address
TMXCC..
creator
36386 PrCmT../8cf01..
owner
36386 PrCmT../8cf01..
term root
b23fa..