Proofgold Term Root Disambiguation

λ x0 . ∃ x1 . and (x1 ∈ omega) (∃ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x1) x3))

as obj
25bca..^{diadic_rational_p}

as prop
-

theory
HotG

stx
7d348..

address
TMFaW..^{diadic_rational_p}