proposition: Lemma hd_red_swap : hd_red (R ++ R') << hd_red (R' ++ R).
proof: Proof. intros x y RR'xy. redtac. ex l r s. repeat split; auto. destruct (in_app_or lr); auto with datatypes. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)