Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 x2 : ι → ο . wceq (cwrecs x0 x1 x2) (cuni (cab (λ x3 . wex (λ x4 . w3a (wfn (cv x3) (cv x4)) (wa (wss (cv x4) x0) (wral (λ x5 . wss (cpred x0 x1 (cv x5)) (cv x4)) (λ x5 . cv x4))) (wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (cfv (cres (cv x3) (cpred x0 x1 (cv x5))) x2)) (λ x5 . cv x4))))))
type
prop
theory
SetMM
name
df_wrecs
proof
PUR6R..
Megalodon
-
proofgold address
TMWEo..
creator
36396 PrCmT../d3590..
owner
36396 PrCmT../d3590..
term root
d394a..