Proofgold Object

λ x0 : ι → (ι → ο) → ο . prim0 (λ x1 . and (∀ x2 : ο . (∀ x3 : ι → ο . x0 x1 x3 ⟶ x2) ⟶ x2) (∀ x2 x3 : ι → ο . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3))

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

theory
HotG

name
DescrR_i_io_1

definition
PUQ2Y..

Megalodon
DescrR_i_io_1

proofgold address
TMG2A..^{DescrR_i_io_1}

creator
4903 Pr6Pc../dea70..

owner
4903 Pr6Pc../dea70..

term root
1d3fd..