proposition: Lemma subenv_stackP e1 e2 : wf_env e2 -> subenv e1 e2 -> exists2 s, stack e2 = s ++ stack e1 & s \subset (blacks e2).
proof: Proof. move=> e2_wf e12; pose n := subenvN e1 e2; exists (take n (stack e2)). by rewrite (subenv_drop e12) // cat_take_drop. by rewrite subenv_take. Qed.
imports: mathcomp(all_ssreflect) bigmin extra