fact: Definition dfs'_correct (dfs' : {set V} -> env -> nat * env) roots e := pre_dfs roots e -> let (m, e') := dfs' roots e in roots \subset blacks e' :|: grays e' /\ post_dfs roots e e' m.
imports: mathcomp(all_ssreflect) extra