Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 : ι → ο . ∀ x4 . x3 x4∀ x5 : ι → ι → ι . (∀ x6 . x6x0∀ x7 . x3 x7x3 (x5 x6 x7))∀ x6 . x6x0x3 (explicit_Nats_primrec x0 x1 x2 x4 x5 x6)
as obj
-
as prop
a23b3..explicit_Nats_primrec_P
theory
HotG
stx
b2e5e..
address
TMPVT..explicit_Nats_primrec_P