Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 : ι → ι . explicit_Nats_primrec x0 x1 x2 x1 (λ x3 x4 . If_i (and (x3 = x1∀ x5 : ο . x5) (340be.. x0 x1 x2 x3 x3)) (x2 x4) x4)
as obj
900a2..
as prop
-
theory
HoTg
stx
f96db..
address
TMXHg..