Proofgold Object

λ x0 x1 x2 x3 . nat_primrec (field3 x0) (λ x4 . field1b x0 (field2b x0 (ap x2 x4) (CRing_with_id_omega_exp x0 x3 x4))) x1

type
ι → ι → ι → ι → ι

theory
HotG

name
CRing_with_id_eval_poly

definition
PUMpo..

Megalodon
CRing_eval_poly

proofgold address
TMTHa..^{CRing_eval_poly}

creator
5881 Pr6Pc../6078b..

owner
5881 Pr6Pc../6078b..

term root
b84ca..