Proofgold Term Root Disambiguation

λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 . and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (∀ x7 . x0 x7 ⟶ ∀ x8 x9 . x1 x7 x4 x8 ⟶ x1 x7 x4 x9 ⟶ x3 x7 x4 x5 x6 x8 = x3 x7 x4 x5 x6 x9 ⟶ x8 = x9)

as obj
4204a..^monic

as prop
-

theory
HotG

stx
2772d..

address
TMQaq..^monic