Proofgold Term Root Disambiguation

MetaFunctor struct_e PtdSetHom (λ x0 . lam_id (ap x0 0)) (λ x0 x1 x2 . lam_comp (ap x0 0)) PtdPred UnaryPredHom (λ x0 . lam_id (ap x0 0)) (λ x0 x1 x2 . lam_comp (ap x0 0)) (λ x0 . unpack_e_i x0 (λ x1 x2 . pack_p x1 (λ x3 . x3 = x2))) (λ x0 x1 x2 . x2)

as obj
-

as prop
1f2a9..^{MetaFunctor_struct_e_struct_p_nonempty}

theory
HotG

stx
5b898..

address
TMXDJ..^{MetaFunctor_struct_e_struct_p_nonempty}