is mentioned by

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]

Try larger context: GenAutomata