Proofgold Object

λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . and (and (prim1 x3 x0) (prim1 x4 x0)) (∀ x5 . prim1 x5 x0 ⟶ explicit_Nats_lt x0 x1 x2 x5 x3 ⟶ explicit_Nats_lt x0 x1 x2 x5 x4 ⟶ x5 = 4ae4a.. 4a7ef..)

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

theory
HoTg

name
-

definition
PUUTm..

Megalodon
-

proofgold address
TMJeZ..

creator
4786 PrGxv../c65cc..

owner
4786 PrGxv../c65cc..

term root
59425..