proposition: Lemma hd_red_mod_union : hd_red_mod E (R ++ R') << hd_red_mod E R U hd_red_mod E R'.
proof: Proof. unfold inclusion. intros. do 2 destruct H. redtac. subst x0. subst y. destruct (in_app_or lr). left. exists (sub s l); split. hyp. apply hd_red_rule. hyp. right. exists (sub s l); split. hyp. apply hd_red_rule. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)