Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . 19c2c.. x1 (λ x2 . λ x3 : ι → ι → ι . 1216a.. 48ef8.. (λ x4 . ∀ x5 : ο . (∀ x6 . and (prim1 x6 (b5c9f.. x2 (4ae4a.. x4))) (∀ x7 . prim1 x7 (4ae4a.. x4)∀ x8 . prim1 x8 (4ae4a.. x4)(x7 = x8∀ x9 : ο . x9)∀ x9 . prim1 x9 (f482f.. x0 4a7ef..)∀ x10 . prim1 x10 (f482f.. x0 4a7ef..)x3 (f482f.. x6 x7) x9 = x3 (f482f.. x6 x8) x10∀ x11 : ο . x11)x5)x5))
as obj
95464..
as prop
-
theory
HoTg
stx
4b82f..
address
TMbZo..