Proofgold Term Root Disambiguation

∀ x0 . atleast6 x0 ⟶ ∃ x1 . and (Subq x1 x0) (and (not (Subq x0 x1)) (atleast5 x1))

as obj
-

as prop
5a74c..^atleast6_E

theory
HF

stx
8a441..

address
TMcHs..^atleast6_E