Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 . nat_primrec x2 (λ x6 . x4 x5)
as obj
77341..
as prop
-
theory
HoTg
stx
32977..
address
TMH1F..explicit_Ring_with_id_exp_nat