Proofgold Term Root Disambiguation

∀ x0 x1 x2 . nIn x2 2 ⟶ ap (setsum x0 x1) x2 = 0

as obj
-

as prop
6a36d..^pair_ap_n2

theory
HotG

stx
08e38..

address
TMJvh..^pair_ap_n2