fact: Definition SCC_tag_fast M t := let oi := find_first (eq t) (eq_dec t) Dom in match oi with | None => None | Some i => match le_gt_dec dim i with | right Hi => @bools_find_first dim (Vnth M Hi) | left _ => None end end.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)