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 : ο . (∀ x4 . and (x4 ∈ x2) (divides_int x1 (x0 x4)) ⟶ x3) ⟶ x3

as obj
-

as prop
2326d..^{Euclid_lemma_Pi_SNo}

theory
HotG

stx
afc5a..

address
TMbrY..^{Euclid_lemma_Pi_SNo}