proposition: Lemma red1_ok : forall t u, red R t u <-> red1 t u.
proof: Proof. intros t u; split; intro H. redtac. ex l r c (cont (s (var l))). subst. rewrite !sub_cont, !fill_fill, !var_fill. split_all. rewrite (term_cont_var (s (var l))) at 1. rewrite fill_fill, comp_comp. refl. rewrite (term_cont_var (s (var r))) at 1. rewrite fill_fill, comp_comp, (rules_preserve_vars_var lr). refl. destruct H as [l]. destruct H as [r]. destruct H as [c]. destruct H as [d]. decomp H. set (s := fun x => if beq_nat x (var l) then fill d (Var (var t)) else Var x). ex l r c s. rewrite H2, H3, !sub_cont. unfold s. rewrite (rules_preserve_vars_var H0), (beq_refl beq_nat_ok), !fill_fill, !comp_comp. tauto. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)