Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 = ap (ap (pack_u x0 x1) 1) x2

as obj
-

as prop
c23d4..^pack_u_1_eq2

theory
HotG

stx
3fdf8..

address
TMF37..^pack_u_1_eq2