Proofgold Term Root Disambiguation

λ x0 x1 . 19c2c.. x0 (λ x2 . λ x3 : ι → ι → ι . 987b2.. (1216a.. x2 (quotient (7a200.. x0 x1))) (λ x4 x5 . canonical_elt (7a200.. x0 x1) (x3 x4 x5)))

as obj
df26d..

as prop
-

theory
HoTg

stx
4b82f..

address
TMahS..