Proofgold Term Root Disambiguation

λ x0 x1 . and (and (x0 ∈ omega) (x1 ∈ omega)) (∀ x2 . x2 ∈ setminus omega 1 ⟶ divides_nat x2 x0 ⟶ divides_nat x2 x1 ⟶ x2 = 1)

as obj
5e7a6..^coprime_nat

as prop
-

theory
HotG

stx
3b6f0..

address
TMFmm..^coprime_nat