Proofgold Term Root Disambiguation

λ x0 x1 x2 x3 . 93c99.. x0 (λ x4 . λ x5 : ι → ι → ι . and (and (prim1 x2 x4) (prim1 x3 x4)) (prim1 (x5 x2 (explicit_Group_inverse x4 x5 x3)) (f482f.. x1 4a7ef..)))

as obj
7a200..

as prop
-

theory
HoTg

stx
4b82f..

address
TMMtc..