Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 : ο . (∀ x6 . and (prim1 x6 x0) (explicit_Nats_one_plus x0 x1 x2 x6 x3 = x4)x5)x5)
as obj
daa5b..
as prop
-
theory
HoTg
stx
f96db..
address
TMVqk..