proposition: Lemma int_red_min : forall R t u, int_red R t u -> min (red R) t -> min (red R) u.
proof: Proof. intros R t u tu. rewrite !min_eq. intros ht f us hu. apply Vforall_intro. intros v hv. apply int_red_pos_eq in tu. destruct tu as [i [f' [hi [ts [hts [w [h1 h2]]]]]]]. ded (ht _ _ hts). clear ht. subst. Funeqtac. subst. destruct (Vin_nth hv) as [j [hj e]]. clear hv. destruct (eq_nat_dec j i); subst. rewrite Vnth_replace. intro hw. assert (NT (red R) (Vnth ts hi)). eapply red_NT. apply h1. hyp. ded (Vforall_nth hi H). contr. rewrite Vnth_replace_neq. 2: lia. intro hv. ded (Vforall_nth hj H). contr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)