Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ Repl (setprod x0 x1) (λ x5 . x2 (ap x5 0) (ap x5 1)) = Repl (setprod x0 x1) (λ x5 . x3 (ap x5 0) (ap x5 1))

as obj
-

as prop
5fe5d..^{ReplEq_setprod_ext}

theory
HF

stx
89549..

address
TMGwK..^{ReplEq_setprod_ext}