Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ x0 ∈ real ⟶ SNoLt 0 x0 ⟶ and (recip_SNo_pos x0 ∈ real) (∀ x1 . nat_p x1 ⟶ and (ap (SNo_recipaux x0 recip_SNo_pos x1) 0 ⊆ real) (ap (SNo_recipaux x0 recip_SNo_pos x1) 1 ⊆ real))

as obj
-

as prop
cfc2e..^{real_recip_SNo_lem1}

theory
HotG

stx
03bd0..

address
TML19..^{real_recip_SNo_lem1}