Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 : ι → ι → ο . λ x1 x2 . ∃ x3 : ι → ι . and (bij (ordsucc x1) x2 x3) (15fbd.. x0 x1 x3)
as obj
f1360..
as prop
-
theory
HotG
stx
ccf27..
address
TMMjd..