fact: Fixpoint shift_rules (p : nat) (R : rules) : rules := match R with | nil => nil | cons a R' => shift_rule p a :: shift_rules (maxvar(lhs a)+p+1) R' end.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)