is mentioned by

Thm* rho:Decl, d:dec(). [[d]] rho Decl	[dec_mng_wf]
Thm* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)	[dec_lookup_monotone]
Thm* ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x)	[dec_lookup_functionality]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Thm* t:dec(). t.typ SimpleType	[dec_typ_wf]
Thm* t:dec(). t.lbl Label	[dec_lbl_wf]
Def dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > >	[dec_lookup]

Try larger context: GenAutomata