proposition: Lemma red_incl_filter_red_rc : red R << filter_ord (red R'%).
proof: Proof. unfold inclusion, filter_ord. intros. redtac. subst x. subst y. elim c; clear c. simpl. right. rewrite !filter_sub. apply red_rule_top. change (In (filter_rule (mkRule l r)) R'). apply in_map. hyp. intros f i j e vi c. set (t := filter (fill c (sub s l))). set (u := filter (fill c (sub s r))). intros htu vj. simpl. rewrite !Vmap_cast, !Vmap_app. simpl. fold t u. set (vi' := Vmap filter vi). set (vj' := Vmap filter vj). destruct htu as [htu|htu]. rewrite htu. left. refl. case (In_dec eq_nat_dec i (map N_val (pi f))); intro Hi. right. destruct (in_map_elim Hi) as [x [hx vx]]. destruct (in_elim hx) as [l1 [l2 hf]]. set (vt := Vcast (Vapp vi' (Vcons t vj')) e). set (vu := Vcast (Vapp vi' (Vcons u vj')) e). assert (a: length l1+length(x::l2)=@arity Sig' f). unfold arity, filter_sig, filter_arity. rewrite hf, length_app. refl. rewrite (Vfilter_app_eq a hf), (Vfilter_app_eq a hf). simpl. set (v1 := Vfilter l1 vu). set (v2 := Vfilter l2 vu). simpl in a. set (d := Cont (Sig:=Sig') f a v1 Hole v2). ded (hyp f). unfold non_dup in H. rewrite hf, map_app in H. simpl in H. destruct (nodup_app_cons H) as [h1 h2]. rewrite <- vx in h1. rewrite <- vx in h2. assert (e1 : Vfilter l1 vt = Vfilter l1 vu). apply Vfilter_eq_notin. intros hi h. ded (in_map N_val h). contr. rewrite e1. assert (e2 : Vfilter l2 vt = Vfilter l2 vu). apply Vfilter_eq_notin. intros hi h. ded (in_map N_val h). contr. rewrite e2. unfold vt, vu. rewrite !Vnth_cast, !Vnth_app. destruct (le_gt_dec i x). 2: lia. repeat (rewrite Vnth_cons_head; [idtac|lia]). change (red R' (fill d t) (fill d u)). apply red_fill. hyp. left. apply args_eq. apply Vfilter_eq_notin with (l:=pi f). intros hi h. ded (in_map N_val h). contr. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)