Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . In x2 x0In (x1 x2) x0)(∀ x2 . In x2 x0∀ x3 . In x3 x0x1 x2 = x1 x3x2 = x3)bij x0 x0 x1
as obj
-
as prop
398e3..PigeonHole_nat_bij
theory
HF
stx
89549..
address
TMVG7..PigeonHole_nat_bij