Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι → ι → ι → ι → ι . (∀ x2 x3 x4 x5 x6 x7 . nth_6_tuple x0 x2 x3 x4 x5 x6 x7 = x1 x2 x3 x4 x5 x6 x7) ⟶ nth_6_tuple x0 = x1

as obj
-

as prop
f957d..

theory
HotG

stx
ddf6a..

address
TMbTE..