Proofgold Term Root Disambiguation

∀ x0 : ι → ι . ∀ x1 . prime_nat x1 ⟶ ∀ x2 . nat_p x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ x0 x3 ∈ int) ⟶ divides_int x1 (05ecb.. x0 x2) ⟶ ∃ x3 . and (x3 ∈ x2) (divides_int x1 (x0 x3))

as obj
-

as prop
2326d..^{Euclid_lemma_Pi_SNo}

theory
HotG

stx
afc5a..

address
TMbrY..^{Euclid_lemma_Pi_SNo}