Proofgold Term Root Disambiguation

∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (Inj0 x4)) ⟶ (∀ x4 . In x4 x1 ⟶ x3 (Inj1 x4)) ⟶ x3 x2

as obj
-

as prop
351c1..^{setsum_Inj_inv_impred}

theory
HF

stx
a6670..

address
TMZKk..^{setsum_Inj_inv_impred}