Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x1∀ x4 : ο . (∀ x5 . and (In x5 x0) (x2 x5 = x3)x4)x4)∀ x3 . In x3 x1and (In (ed93b.. x0 x2 x3) x0) (x2 (ed93b.. x0 x2 x3) = x3)
as obj
-
as prop
98109..surj_rinv
theory
HF
stx
e311e..
address
TMcAC..surj_rinv