is mentioned by

Thm* t:eff(). t.smt smt()	[eff_smt_wf]
Thm* t:smt(). t.typ SimpleType	[smt_typ_wf]
Thm* t:smt(). t.term Term	[smt_term_wf]
Thm* t:smt(). t.lbl Label	[smt_lbl_wf]
Thm* SQType(smt())	[smt_sq]
Def eff() == LabelLabelSimpleTypesmt()	[eff]
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 smt_terms(c) == < s.term | s c >	[smt_terms]

Try larger context: GenAutomata