Proofgold Term Root Disambiguation

setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2)

as obj
-

as prop
ed37d..^{pair_tuple_fun}

theory
HotG

stx
08e38..

address
TMQLy..^{pair_tuple_fun}