Proofgold Term Root Disambiguation

λ x0 : ι → ι → ο . λ x1 . and (x0 x1 x1) (x1 = canonical_elt x0 x1)

as obj
5a423..

as prop
-

theory
HoTg

stx
db9a4..

address
TMQga..^quotient