proposition: Lemma stackE e : wf_env e -> stack e = seen e :\: cover (esccs e).
proof: Proof. move=> e_wf; apply/setP=> x; rewrite seenE// setDUl setDv setU0. by rewrite !inE -num_sccs// -num_lt_V//; case: ltngtP. Qed.
imports: mathcomp(all_ssreflect) bigmin extra