proposition: Lemma red_incl_shift_red : red R << red R'.
proof: Proof. unfold inclusion. intros. redtac. ded (hyp lr). destruct H as [p]. rewrite (sub_shift p l) in xl. subst x. assert (incl (vars r) (vars l)). apply hyp0. hyp. rewrite (sub_shift_incl p s H0) in yr. subst y. apply red_rule. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)