Proofgold Object

λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . bij x1 x1))

type
ι → ο

theory
HotG

name
Permutation

definition
PUfuv..

Megalodon
struct_u_bij

proofgold address
TMQ6z..^struct_u_bij

creator
9725 PrCx1../d8141..

owner
9725 PrCx1../d8141..

term root
4f4ed..