fact: Record wf_env e := WfEnv { serialE : serial e = sn e; sub_gsccs : esccs e \subset gsccs; max_num : forall x, num e x <= infty; num_lt_V_is_stack : forall x, num e x < #|V| -> num e x < sn e; num_sccs : forall x, (num e x == #|V|) = (x \in cover (esccs e)); le_connect : forall x y, num e x <= num e y < sn e -> gconnect x y; }.
imports: mathcomp(all_ssreflect) bigmin extra