proposition: Lemma WF_red_mod_flat : WF (red_mod E R) <-> WF (red_mod (flat_rules E) (flat_rules R)).
proof: Proof. split; intro. intro t. gen (H t). induction 1. apply SN_intro; intros. apply H1. do 2 destruct H2. exists x0. split. eapply incl_elim. eapply rtc_incl. apply red_flat. hyp. apply red_flat. hyp. intro t. geneq H t (fill one_flat_cont t). induction 1. intros. subst. apply SN_intro; intros. apply H0 with (fill one_flat_cont y). 2: refl. do 2 destruct H1. exists (fill one_flat_cont x). split. apply rtc_red_one_flat_cont_intro; hyp. apply red_one_flat_cont_intro; hyp. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)