proposition: Lemma red_incl_proj_red_rc : red R << proj_ord (red R' %).
proof: Proof. unfold inclusion, proj_ord. intros. redtac. subst. elim c. simpl. right. rewrite !proj_sub. apply red_rule_top. change (In (proj_rule (mkRule l r)) R'). apply in_map. hyp. intros. simpl. case (pi f). intros [k h]. rewrite !Vnth_cast, !Vnth_app. case (le_gt_dec i k); intro. case (eq_nat_dec i k); intro. subst. repeat (rewrite Vnth_cons_head; [idtac|lia]). hyp. gen (Vnth_app_aux (S j) (Vnth_cast_aux e h) l0). assert (k-i=S(k-i-1)). lia. rewrite H0. intro. rewrite !Vnth_cons. left. refl. left. refl. rewrite !Vmap_cast, !Vmap_app. simpl. destruct H. rewrite H. left. refl. right. set (d := Cont f e (Vmap proj t) Hole (Vmap proj t0)). set (t1 := proj (fill c0 (sub s l))). set (u := proj (fill c0 (sub s r))). change (red R' (fill d t1) (fill d u)). apply red_fill. hyp. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil SN ARelation RelUtil ACompat NatUtil)