proposition: Lemma int_red_incl_red : int_red R << red R.
proof: Proof. unfold inclusion, int_red. intros. decomp H. subst x. subst y. apply red_rule. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)