proposition: Lemma red_one_flat_cont_intro : red R << red_flat_cont.
proof: Proof. intros t u h. redtac. subst. unfold red_flat_cont, Rof. rewrite !fill_fill. case_eq (is_root_preserving (mkRule l r)); intros. apply red_rule. unfold flat_rules. rewrite in_flat_map. exists (mkRule l r). split_all. unfold flat_rule. rewrite H. simpl. auto. destruct l. discr. destruct r. discr. destruct (cont_case (comp one_flat_cont c)). discr. destruct H0 as [d [g [i [vi [j [vj [e]]]]]]]. rewrite !H0, <- !fill_fill. set (l := Fun f t). set (r := Fun f0 t0). apply context_closed_red. assert (m : maxvar_rule (mkRule l r) < S n). eapply maxvar_rules_elim. apply lr. lia. rewrite !fill_sub with (n:=n). set (s' := maxvar_union (S n) s (fsub n (Vapp vi vj))). apply hd_red_incl_red. apply hd_red_rule. unfold flat_rules. rewrite in_flat_map. exists (mkRule l r). split_all. unfold flat_rule. unfold l, r. rewrite H, in_map_iff. assert (h : i < arity g). lia. exists (flat_cont_symb (S n) h). split_all. simpl. gen (flat_cont_aux h). assert (arity g - S i = j). lia. rewrite H1. intro. assert (e0=e). apply eq_unique. subst. refl. unfold flat_conts. rewrite in_flat_map. exists g. split. apply Fs_ok. unfold flat_conts_symb. rewrite in_map_iff. exists (N_ h). split_all. apply In_L. trans (maxvar_rule (mkRule l r)). lia. apply Nat.le_max_r. trans (maxvar_rule (mkRule l r)). lia. apply Nat.le_max_l. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)