proposition: Lemma WF_red0 : WF (red R) <-> WF (red0 R).
proof: Proof. split; intro. apply (WF_incl (red R)). intros t u. unfold red0. intuition. hyp. cut (forall t, SN (red0 R) t -> maxvar t = 0 -> forall x, SN (red R) (sub (single 0 (@Var Sig x)) t)). intro. intro u. rewrite (term_sub_cont 0 u). apply H0. apply H. rewrite maxvar_fill. refl. induction 1. intros h v. apply SN_intro; intros. destruct (red_ren (is_ren_single_var 0 v) hR H2). destruct H3. subst. assert (red0 R x x0). unfold red0. intuition. apply H1. hyp. eapply red0_maxvar. apply H4. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)