proposition: Lemma notin_vars_shift x l : ~In x (vars (shift l)) -> p <= x -> ~In (x-p) (vars l).
proof: Proof. intros h1 h2 h3. apply h1. rewrite vars_shift, <- (le_minus_plus h2). fold (shift_var (x-p)). apply in_map. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)