Proofgold Term Root Disambiguation

λ x0 . λ x1 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x1 (nth_6_tuple (ap x0 0)) (nth_6_tuple (ap x0 u1))

as obj
4aafd..

as prop
-

theory
HotG

stx
ddf6a..

address
TMLuC..