Proofgold Object

λ x0 . unpack_u_i x0 (λ x1 . λ x2 : ι → ι . lam (setprod int x1) (λ x3 . If_i (SNoLt (ap x3 0) 0) (1319b.. (minus_SNo (ap x3 0)) (inv x1 x2) (ap x3 1)) (1319b.. (ap x3 0) x2 (ap x3 1))))

type
ι → ι

theory
HotG

name
-

definition
PULps..

Megalodon
-

proofgold address
TMZbo..

creator
35061 PrKYB../4bb89..

owner
35061 PrKYB../4bb89..

term root
3777f..