Proofgold Proposition

∀ x0 x1 . proj1 (setsum x0 x1) = x1

type
prop

theory
HotG

name
proj1_pair_eq

proof
PUMB7..

Megalodon
proj1_pair_eq

proofgold address
TMM7L..^{proj1_pair_eq}

creator
4898 Pr6Pc../94ff4..

owner
4898 Pr6Pc../94ff4..

term root
9f98a..