proposition: Lemma hd_red_SCC'_cover t1 t2 : hd_red R t1 t2 -> exists i, hd_red_SCC' i t1 t2 /\ i<dim.
proof: Proof. intros. unfold hd_red in *. do 4 destruct H; destruct H0. cut (exists n, SCC'_tag HM (mkRule x x0) = Some n). intro. destruct H2 as [i]. exists i. split. exists x; exists x0; exists x1. split; try tauto. apply (find_first_Some_bound (SCC' (mkRule x x0)) (SCC'_dec HM (mkRule x x0))). intuition. ded (find_first_exist (SCC' (mkRule x x0)) (SCC'_dec HM (mkRule x x0)) _ R H). assert (SCC'_tag HM (mkRule x x0) <> None). apply H2. split; try tauto. left; auto. destruct (SCC'_tag HM (mkRule x x0)). exists n; auto. congruence. Qed.
imports: Coq(Permutation Multiset Setoid PermutSetoid) CoLoR(SCCTopoOrdering AGraph ATrs RelUtil RelSub BoundNat AdjMat LogicUtil NatUtil SCC SCC_dec ListExtras SN VecUtil GDomainBij OptUtil Union SortUtil ListNodup ListPermutation)