Search for blocks/addresses/...

Proofgold Term Root Disambiguation

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