Proofgold Term Root Disambiguation

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

as obj
-

as prop
6e7a2..^{pair_tuple_fun}

theory
HF

stx
89549..

address
TMQn1..^{pair_tuple_fun}