Proofgold Term Root Disambiguation

SNo_rec_i (λ x0 . λ x1 : ι → ι . SNoCut (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 1)))

as obj
2f4ee..^{recip_SNo_pos}

as prop
-

theory
HotG

stx
87341..

address
TMNiA..^{recip_SNo_pos}