fact: Record wf_env e := WfEnv { wf_stack : stack e =i grays e :|: (blacks e :\: cover (esccs e)); wf_sccs : cover (esccs e) \subset blacks e; wf_uniq : uniq (stack e) }.
imports: mathcomp(all_ssreflect) bigmin extra