Proofgold Object

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

type
ι → ι → ο

theory
HotG

name
SNo_max_of

definition
PUesu..

Megalodon
SNo_max_of

proofgold address
TMZxc..^SNo_max_of

creator
12391 PrGxv../f8c0c..

owner
12391 PrGxv../f8c0c..

term root
9570d..