Proofgold Term Root Disambiguation

λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . If_i (x0 x2 (x1 x2)) (x1 x2) (canonical_elt x0 x2)

as obj
35d1d..

as prop
-

theory
HoTg

stx
db9a4..

address
TMXTW..^{canonical_elt_def}