fact: Record invariants (e : env) := Invariants { pre_wf_env : wf_env e; pre_wf_graph : wf_graph e; wf_noblack_towhite : noblack_to_white e; pre_sccs : esccs e = black_gsccs e; }.
imports: mathcomp(all_ssreflect) bigmin extra