Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 x3 : ι → ι → ι . λ x4 . prim0 (λ x5 . and (prim1 x5 x0) (x2 x4 x5 = x1))

as obj
70d5f..

as prop
-

theory
HoTg

stx
32977..

address
TMaKR..^{explicit_Ring_minus}