Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
as obj
-
as prop
be11a..nat_primrec_0
theory
HotG
stx
d0fc7..
address
TMVRM..nat_primrec_0