Proofgold Term Root Disambiguation

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

as obj
9fe6a..^idR

as prop
-

theory
HotG

stx
2772d..

address
TMHFU..^idR