Proofgold Proposition

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

type
prop

theory
HotG

name
Sing_nat_fresh_extension

proof
PUQvq..

Megalodon
Sing_nat_fresh_extension

proofgold address
TMZ6h..^{Sing_nat_fresh_extension}

creator
28444 PrQUS../b6bac..

owner
28444 PrQUS../b6bac..

term root
18d72..