Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ SNo (x1 x2)

as obj
7ed8b..^SNo_ord_seq

as prop
-

theory
HotG

stx
26642..

address
TMcDS..^SNo_ord_seq