Proofgold Term Root Disambiguation

∀ x0 x1 . setsum_p x0 ⟶ In x0 x1 ⟶ In (ap x0 1) (ap x1 (ap x0 0))

as obj
-

as prop
f8570..^{setsum_p_In_ap}

theory
HF

stx
89549..

address
TMLax..^{setsum_p_In_ap}