Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ο . (∀ x1 . x0 x1∀ x2 . x0 x2x0 (setsum x1 x2))∀ x1 : ο . (∀ x2 : ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x9 . lam x9 (λ x10 . x10)) (λ x9 x10 x11 x12 x13 . lam x9 (λ x14 . ap x12 (ap x13 x14))) x2 x4 x6 x8x7)x7)x5)x5)x3)x3)x1)x1
as obj
-
as prop
3c078..MetaCatSet_coproduct_gen
theory
HotG
stx
2772d..
address
TMbUm..MetaCatSet_coproduct_gen