Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x2setsum x0 x1or (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = Inj0 x4)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x1) (x2 = Inj1 x4)x3)x3)
as obj
-
as prop
a3640..setsum_Inj_inv
theory
HotG
stx
114a5..
address
TMGJo..setsum_Inj_inv