fact: Definition dfs1 (dfs' : {set V} -> env -> nat * env) (x : V) e := let m := rank x (x :: stack e) in let: (m1, e1) := dfs' [set y in successors x] (add_stack x e) in if m1 < m then (m1, add_blacks x e1) else (infty, add_sccs x e1).
imports: mathcomp(all_ssreflect) extra