Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2lam x0 x1) (∀ x3 : ο . (∀ x4 . and (x4x0) (∀ x5 : ο . (∀ x6 . and (x6x1 x4) (x2 = setsum x4 x6)x5)x5)x3)x3)
as obj
-
as prop
e7bf4..lamEq
theory
HotG
stx
08e38..
address
TMXKo..lamEq