Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∃ x1 . and (prime_nat x1) (divides_nat x1 x0)

as obj
-

as prop
979fd..^{prime_nat_divisor_ex}

theory
HotG

stx
00571..

address
TMS8E..^{prime_nat_divisor_ex}