Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ο . λ x2 . prim0 (λ x3 . and (x1 x3) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) x3))

as obj
e1c3c..^CD_proj1

as prop
-

theory
HotG

stx
4317c..

address
TMVCf..^CD_proj1