is mentioned by
| 
 Def col_subst2(c;r)
== col_map_subst(as.rel_subst2(as;r); < zip(rel_primed_vars(r);s) | 
 s  | [col_subst2] | 
| 
 Def col_subst(c;r)
== col_map_subst(as.rel_subst(as;r); < zip(rel_vars(r);s) | s  | [col_subst] | 
| 
 Def pred_unprime(P) ==  < rel_unprime(r) | r  | [pred_unprime] | 
In prior sections: mb collection mb automata 2
Try larger context: GenAutomata