Proofgold Term Root Disambiguation

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

as obj
27421..^idL

as prop
-

theory
HotG

stx
2772d..

address
TMHaC..^idL