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. simpl. right. rewrite !filter_sub. apply red_rule_top. change (In (filter_rule (mkRule l r)) R'). apply in_map. hyp. intros. set (bs := Vbreak (n1:=i) (n2:=S j) (Vcast (pi f) (sym_eq e))). case_eq (Vhead (snd bs)); intro H0. rewrite (filter_cont_true f e t c0 t0 (sub s l) H0). rewrite (filter_cont_true f e t c0 t0 (sub s r) H0). fold bs. destruct H. left. simpl fill. rewrite H. refl. right. apply red_fill. hyp. left. rewrite (filter_cont_false f e t c0 t0 (sub s l) H0). rewrite (filter_cont_false f e t c0 t0 (sub s r) H0). refl. Qed.
imports: CoLoR(ATrs VecFilter VecUtil LogicUtil RelUtil SN NatUtil ARelation ACompat) Coq(List)