Proofgold Proposition

∀ x0 . setsum 1 x0 = Inj1 x0

type
prop

theory
HotG

name
Inj1_setsum_1L

proof
PUMB7..

Megalodon
Inj1_setsum_1L

proofgold address
TMME8..^{Inj1_setsum_1L}

creator
4898 Pr6Pc../9d72d..

owner
4898 Pr6Pc../9d72d..

term root
f8d72..