Proofgold Term Root Disambiguation

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

as obj
-

as prop
e0cb0..^{proj1_pair_eq}

theory
HotG

stx
114a5..

address
TMLxP..^{proj1_pair_eq}