is mentioned by

Thm* r:rel(), as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst2(as;r);ds;da;de)	[rel_subst2_tc]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))	[member_col_subst2]
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r))	[rel_primed_vars_rel_vars]
Thm* r:rel(). rel_primed_vars((r)') = rel_vars(r)	[rel_vars_addprime]
Thm* x:Label, r:rel(). (x rel_primed_vars(r)) (i:. i < ||r.args|| & (x term_primed_vars(r.args[i])))	[member_rel_primed_vars]
Def col_subst2(c;r) == col_map_subst(as.rel_subst2(as;r); < zip(rel_primed_vars(r);s) | s col_list_prod(map(c;rel_primed_vars(r))) > )	[col_subst2]

Try larger context: GenAutomata