Proofgold Term Root Disambiguation

∀ x0 : ι → ο . x0 (Inj0 0) ⟶ x0 (Inj0 (Power 0)) ⟶ (∀ x1 x2 . combinator x1 ⟶ x0 x1 ⟶ combinator x2 ⟶ x0 x2 ⟶ x0 (Inj1 (setsum x1 x2))) ⟶ ∀ x1 . combinator x1 ⟶ x0 x1

as obj
-

as prop
69124..^{combinator_ind}

theory
HF

stx
2b38c..

address
TMHrx..^{combinator_ind}