Proofgold Term Root Disambiguation

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

as obj
-

as prop
b57b6..^{unpack_e_o_eq}

theory
HotG

stx
3fdf8..

address
TMJs5..^{unpack_e_o_eq}