is mentioned by

Thm* p:Fmla, ss:Collection(smt()). smts_eff_pred(ss;p) Fmla

[smts_eff_pred_wf]

In prior sections: mb automata 2

Try larger context: GenAutomata