Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . (∀ x1 . x1 ⊆ u12 ⟶ atleastp u5 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ⊆ u16 ⟶ atleastp u6 x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3)) ⟶ atleastp u2 (setminus x1 u12)

as obj
-

as prop
a62ab..

theory
HotG

stx
2d143..

address
TMVDv..