is mentioned by

Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) tc(rel_unprime(r);ds;da;de)	[tc_unprime]
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr	[rel_mng_2_unprime]
Thm* r:rel(), e,a,s,ds,da,de,rho,tr:Top. [[r]] rho ds da de e s a tr ~ [[rel_unprime(r)]] rho ds da de e s a tr	[rel_mng_unprime]
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 pred_unprime(P) == < rel_unprime(r) | r P >	[pred_unprime]

Try larger context: GenAutomata