Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . prim1 x8 x6 ⟶ ∀ x9 : ο . (∀ x10 . prim1 x10 x2 ⟶ ∀ x11 . prim1 x11 x3 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ (∀ x10 . prim1 x10 x4 ⟶ ∀ x11 . prim1 x11 x5 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . prim1 x8 x2 ⟶ ∀ x9 . prim1 x9 x3 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7) ⟶ (∀ x8 . prim1 x8 x4 ⟶ ∀ x9 . prim1 x9 x5 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7) ⟶ Subq x6 x7

as obj
-

as prop
b4f65..

theory
HoTg

stx
2624a..

address
TMMoA..