fact: Definition ren_cap (r1 r2 : rule) := ren_cap R (S (maxvar (lhs r2))) (rhs r1).
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)