Proofgold Object

λ x0 . and (struct_b_b_e x0) (unpack_b_b_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 . explicit_Ring x1 x4 x2 x3))

type
ι → ο

theory
HotG

name
Ring

definition
PUajT..

Megalodon
Rng

proofgold address
TMVey..^Rng

creator
4949 Pr6Pc../bc6d2..

owner
4949 Pr6Pc../bc6d2..

term root
61bbe..