Proofgold Term Root Disambiguation

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

as obj
-

as prop
0c12f..^{proj0_pair_eq}

theory
HotG

stx
114a5..

address
TMbPL..^{proj0_pair_eq}