Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . prim1 x5 x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0

as obj
-

as prop
e2782..

theory
HoTg

stx
ee211..

address
TMV6d..^{nat_primrec_r}