proposition: Lemma grays_add_sccs e x : let s := take (index x (stack e)) (stack e) in uniq (stack e) -> s \subset blacks e -> x \in grays e -> grays (add_sccs x e) = grays e :\ x.
proof: Proof. move=> /= se_uniq sb x_gray; rewrite /add_sccs /grays /=. case: path.splitP sb se_uniq; first by rewrite grays_stack. move=> s s' sb sxs'_uniq. apply/setP=> y; rewrite !inE mem_cat mem_rcons in_cons. have [->|] //= := altP eqP; rewrite orbC ![(y \notin _) && _]andbC. have [|yNs' neq_yx] //= := boolP (y \in s'). by have [y_s|] //= := boolP (y \in s); rewrite (subsetP sb). Qed.
imports: mathcomp(all_ssreflect) extra