proposition: Lemma WF_red_mod0 : WF (red_mod E R) <-> WF (red_mod0 E R).
proof: Proof. split; intro. apply (WF_incl (red_mod E R)). intros t u. unfold red_mod0. intuition. hyp. cut (forall t, SN (red_mod0 E R) t -> maxvar t = 0 -> forall x, SN (red_mod E 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_mod_ren (is_ren_single_var 0 v) hE hR H2). destruct H3. subst. assert (red_mod0 E R x x0). unfold red_mod0. split_all. apply H1. hyp. eapply red_mod0_maxvar. apply H4. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)