Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ SNoLt 0 x2 ⟶ and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1)) ⟶ SNoCutP (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 1))

as obj
-

as prop
c6f6d..^{SNo_recipaux_lem2}

theory
HotG

stx
87341..

address
TMZp1..^{SNo_recipaux_lem2}