proposition: Lemma shift_rules_lhs : forall R p, map lhs (shift_rules p R) = shift_terms p (map lhs R).
proof: Proof. induction R; simpl; intros. refl. destruct a. simpl. apply tail_eq. apply IHR. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)