is mentioned by

Thm* t:eff(). t.smt smt()	[eff_smt_wf]
Thm* t:eff(). t.typ SimpleType	[eff_typ_wf]
Thm* t:eff(). t.kind Label	[eff_kind_wf]
Def action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs | a f.acts > >	[action_effect]
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