is mentioned by

Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)	[closed_tapp]
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)	[member_st_app]
Def pred_mentions(p;x) == r:rel(). r p & rel_mentions(r;x)	[pred_mentions]
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]

In prior sections: core int 1 bool 1 int 2 mb nat num thy 1 mb list 1 mb collection mb list 2 fun 1 rel 1

Try larger context: GenAutomata