Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ι . ∀ x1 x2 . unpack_e_i (pack_e x1 x2) x0 = x0 x1 x2

as obj
-

as prop
98c7f..^{unpack_e_i_eq}

theory
HotG

stx
3fdf8..

address
TMXmw..^{unpack_e_i_eq}