Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = x1 x3 x2

as obj
af600..

as prop
-

theory
HoTg

stx
4b82f..

address
TMSbR..^{explicit_abelian}