proposition: Lemma WF_red_flat : WF (red R) <-> WF (red (flat_rules R)).
proof: Proof. split; intro. intro t. gen (H t). induction 1. apply SN_intro; intros. apply H1. 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. apply red_one_flat_cont_intro. hyp. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)