Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2∀ x3 : ο . (inj x0 x1 x2(∀ x4 . In x4 x1∃ x5 . and (In x5 x0) (x2 x5 = x4))x3)x3
as obj
-
as prop
80a11..bijE_impred
theory
HF
stx
89549..
address
TMFBf..bijE_impred