is mentioned by

Def smts_eff(ss;x) == smt_terms( < s ss | s.lbl = x > )	[smts_eff]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))	[covers_var]

Try larger context: GenAutomata