proposition: Lemma red_reset : forall t u, red R t u <-> red (reset_rules R) t u.
proof: Proof. split; intro. redtac. subst. ded (rules_preserve_vars_var hR lr). case (In_dec eq_nat_dec 0 (vars l)); intro. rewrite vars_var in i. simpl in i. split_all. apply red_rule. assert (mkRule l r = reset_rule (mkRule l r)). unfold reset_rule. simpl. unfold reset. rewrite H, !H0, !swap_id. refl. rewrite H1. apply in_map. hyp. rewrite swap_intro with (x:=var l)(y:=0). 2: hyp. rewrite swap_intro with (t:=r)(x:=var r)(y:=0). 2:{ rewrite vars_var. rewrite vars_var in n. rewrite H. hyp. } rewrite H at -2. apply red_rule. change (In (reset_rule (mkRule l r)) (reset_rules R)). apply in_map. hyp. redtac. rename l into l0. rename r into r0. subst. destruct (in_map_elim lr). destruct H. destruct x as [l r]. unfold reset_rule in H0. simpl in H0. inversion H0. unfold reset. rewrite !sub_sub. ded (rules_preserve_vars_var hR H). rewrite H1. apply red_rule. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)