proposition: Lemma red_flat : red (flat_rules R) << red R.
proof: Proof. intros t u h. redtac. unfold flat_rules in lr. rewrite in_flat_map in lr. destruct lr as [[a b] [h1 h2]]. unfold flat_rule in h2. simpl in h2. destruct a. simpl in h2. split_all. inversion H. subst. apply red_rule. hyp. destruct b. simpl in h2. split_all. inversion H. subst. apply red_rule. hyp. revert h2. case_beq_symb Sig f f0; intro. simpl in h2. split_all. inversion H. subst. apply red_rule. hyp. rewrite in_map_iff in h2. destruct h2 as [d [h3 h4]]. unfold flat_cont_rule in h3. inversion h3. clear h3. subst. unfold flat_conts in h4. rewrite in_flat_map in h4. destruct h4 as [g [h5 h6]]. unfold flat_conts_symb in h6. rewrite in_map_iff in h6. destruct h6 as [x [h3 h4]]. subst. unfold flat_cont_symb. simpl. rewrite !Vmap_cast, !Vmap_app. simpl. set (v1 := Vmap (sub s) (fresh (S n) x)). set (v2 := Vmap (sub s) (fresh (S(n+x)) (arity g - S x))). set (e := flat_cont_aux x). set (d' := Cont g e v1 Hole v2). set (v' := Vmap (sub s) t0). set (v0' := Vmap (sub s) t1). change (red R (fill c (fill d' (sub s (Fun f t0)))) (fill c (fill d' (sub s (Fun f0 t1))))). rewrite !fill_fill. apply red_rule. hyp. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)