Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 : ο . (∀ x2 . and (prime_nat x2) (divides_nat x2 x0) ⟶ x1) ⟶ x1

as obj
-

as prop
979fd..^{prime_nat_divisor_ex}

theory
HotG

stx
00571..

address
TMS8E..^{prime_nat_divisor_ex}