Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ι → ι . ∀ x1 x2 x3 . unpack_e_e_i (pack_e_e x1 x2 x3) x0 = x0 x1 x2 x3

as obj
-

as prop
d2638..

theory
HotG

stx
a8341..

address
TMU2w..