Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ο . λ x2 : ι → ι . λ x3 . pair_tag x0 (x2 (CD_proj0 x0 x1 x3)) (x2 (CD_proj1 x0 x1 x3))

as obj
87e4d..^CD_minus

as prop
-

theory
HotG

stx
4317c..

address
TMHa9..^CD_minus