Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq crng (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) csgrp) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (co (cv x4) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (co (co (cv x4) (cv x5) (cv x3)) (co (cv x4) (cv x6) (cv x3)) (cv x2))) (wceq (co (co (cv x4) (cv x5) (cv x2)) (cv x6) (cv x3)) (co (co (cv x4) (cv x6) (cv x3)) (co (cv x5) (cv x6) (cv x3)) (cv x2)))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . cabl))
as obj
-
as prop
334fc..
theory
SetMM
stx
10cbd..
address
TMMbE..