Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . ∃ x1 . and (prim1 x1 48ef8..) (∃ x3 . and (and (and (and (∀ x5 . prim1 x5 (4ae4a.. x1)4f2b4.. (f482f.. x3 x5)) (∀ x5 . prim1 x5 x121582.. (f482f.. x3 x5) (f482f.. x3 (4ae4a.. x5)))) (∀ x5 . prim1 x5 x1eb6e9.. (df26d.. (f482f.. x3 (4ae4a.. x5)) (f482f.. x3 x5)))) (x0 = f482f.. x3 x1)) (70df3.. (f482f.. x3 4a7ef..)))
as obj
173cc..
as prop
-
theory
HoTg
stx
4b82f..
address
TMTPt..