fact: Definition shift_inv_var x := match le_lt_dec p x with | left _ => if Inb eq_nat_dec (x-p) (vars l) then x-p else x | right _ => x end.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)