proposition: Lemma shift_red_incl_red : red R' << red R.
proof: Proof. unfold inclusion. intros. redtac. rename l into l'. rename r into r'. subst x. subst y. ded (hyp lr). do 3 destruct H. destruct x0 as [l r]. simpl in H0. inversion H0. subst l'. subst r'. unfold shift. rewrite !sub_sub. apply red_rule. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)