Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ recip_SNo_pos x0 = SNoCut (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 1))

as obj
-

as prop
ebab7..^{recip_SNo_pos_eq}

theory
HotG

stx
87341..

address
TMX3p..^{recip_SNo_pos_eq}