proposition: Lemma SCC'_list_aux_exact : forall i L r, In r (SCC'_list_aux i L) <-> In r L /\ SCC'_tag HM r = Some i.
proof: Proof. intros. induction L. simpl in *. tauto. split; intro. simpl in *. destruct (eq_opt_dec eq_nat_dec (SCC'_tag HM a) (Some i)); destruct (rule_eq_dec a r); simpl in *; intuition. subst a; tauto. destruct H. simpl in *. destruct (eq_opt_dec eq_nat_dec (SCC'_tag HM a) (Some i)); destruct H; simpl in *; try subst a; tauto. 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)