Proofgold Term Root Disambiguation

λ x0 x1 . ∃ x2 . and (and (∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x1) (prim1 (7ee77.. x4 x5) x2)) (∀ x4 . prim1 x4 x1 ⟶ ∃ x5 . and (prim1 x5 x0) (prim1 (7ee77.. x5 x4) x2))) (∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) x2 ⟶ prim1 (7ee77.. x6 x7) x2 ⟶ iff (x4 = x6) (x5 = x7))

as obj
c2e41..

as prop
-

theory
HoTg

stx
f69d8..

address
TMQ55..