Proofgold Term Root Disambiguation

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

as obj
-

as prop
db889..

theory
HotG

stx
a8341..

address
TMYWC..