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_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst(as;r);ds;da;de)	[rel_subst_tc]
Thm* c:(LabelCollection(Term)), r,r':rel(). r' col_subst(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst(as;r))	[member_col_subst]
Thm* r:rel(), as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r)	[trivial_rel_subst]
Def col_subst(c;r) == col_map_subst(as.rel_subst(as;r); < zip(rel_vars(r);s) | s col_list_prod(map(c;rel_vars(r))) > )	[col_subst]

In prior sections: mb automata 2

Try larger context: GenAutomata