Proofgold Term Root Disambiguation

λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (∀ x3 : ο . (∀ x4 . and (x4 ∈ int) (x0 = mul_SNo (eps_ x2) x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1

as obj
25bca..^{diadic_rational_p}

as prop
-

theory
HotG

stx
7d348..

address
TMFaW..^{diadic_rational_p}