Proofgold Term Root Disambiguation

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

as obj
-

as prop
d6e1a..^{proj0_pair_eq}

theory
HF

stx
cbc45..

address
TMLPR..^{proj0_pair_eq}