fact: Fixpoint shift_terms (p : nat) (l : list term) : list term := match l with | nil => nil | cons t l' => shift p t :: shift_terms (maxvar t + p + 1) l' end.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)