Proofgold Object

λ x0 x1 . and (and (x1 ∈ x0) (SNo x1)) (∀ x2 . x2 ∈ x0 ⟶ SNo x2 ⟶ SNoLe x1 x2)

type
ι → ι → ο

theory
HotG

name
SNo_min_of

definition
PUesu..

Megalodon
SNo_min_of

proofgold address
TMMJU..^SNo_min_of

creator
12391 PrGxv../b7e6c..

owner
12391 PrGxv../b7e6c..

term root
5eb8d..