Proofgold Object

λ x0 : ι → ο . λ x1 . λ x2 : ι → ι . ∀ x3 . x3 ∈ x1 ⟶ and (x0 (x2 x3)) (∀ x4 . x4 ∈ x3 ⟶ SNoLe (x2 x3) (x2 x4))

type
(ι → ο) → ι → (ι → ι) → ο

theory
HotG

name
-

definition
PUQQ9..

Megalodon
nonincrfinseq

proofgold address
TMUcd..^{nonincrfinseq}

creator
30111 PrQUS../1c9a8..

owner
30111 PrQUS../1c9a8..

term root
f77d4..