is mentioned by

Thm* t:sm{i:l}(). t.ds Decl	[sm_ds_wf]
Thm* t:sm{i:l}(). t.da Decl	[sm_da_wf]
Def sm{i:l}() == da:Declds:Decl({ds}Prop)({ds}(da){ds}Prop)	[sm]

In prior sections: mb declaration mb record

Try larger context: GenAutomata