Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι . λ x2 . Eps_i (λ x3 . and (In x3 x0) (x1 x3 = x2))
as obj
ed93b..inv
as prop
-
theory
HF
stx
e311e..
address
TMWaB..inv