Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ {x2 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1} = {x3 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1}

as obj
-

as prop
f689a..^{ReplEq_setprod_ext}

theory
HotG

stx
d9726..

address
TMWwk..^{ReplEq_setprod_ext}