proposition: Lemma int_red_rtc_min : forall R t u, int_red R # t u -> min (red R) t -> min (red R) u.
proof: Proof. induction 1; intro hx. eapply int_red_min. apply H. hyp. hyp. apply IHclos_refl_trans2. apply IHclos_refl_trans1. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)