is mentioned by

Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Def single_valued_decls(c) == x:Label, t1,t2:SimpleType. mk_dec(x, t1) c mk_dec(x, t2) c t1 = t2	[single_valued_decls]

Try larger context: GenAutomata