Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ 1 ∈ x0 ⟶ ∀ x1 . ExtendedSNoElt_ x0 x1 ⟶ ∀ x2 . x2 ∈ x1 ⟶ nIn (Sing x0) x2

as obj
-

as prop
a0507..^{Sing_nat_fresh_extension}

theory
HotG

stx
5ed1a..

address
TMWBw..^{Sing_nat_fresh_extension}