proposition: Lemma colorP x e : wf_env e -> color_spec x e (x \in blacks e) (x \in stack e) (x \in cover (esccs e)) (x \in grays e) (x \in whites e).
proof: Proof. move=> [/setP /(_ x) s_def] /subsetP /(_ x) /implyP. move: s_def; rewrite /grays /whites !inE. case x_black: (_ \in blacks _) => /=; case x_stack : (_ \in stack _) => /=; case x_sccs : (_ \in cover _) => //=; do ?by constructor. by constructor=> //; rewrite /grays !inE x_black. by constructor; rewrite /whites !inE x_black x_stack. Qed.
imports: mathcomp(all_ssreflect) extra