proposition: Lemma subenv_take e1 e2 : wf_env e2 -> subenv e1 e2 -> take (subenvN e1 e2) (stack e2) \subset blacks e2.
proof: Proof. set n := subenvN e1 e2; move=> e2_wf e12; apply/subsetP=> x x_p2. suff: (x \in stack e2) && (x \notin grays e2) by case: colorP. rewrite (mem_take x_p2) (subenv_grays e12) /=. apply: contraTN isT => /grays_stack. have := wf_uniq e2_wf; rewrite -[stack e2](cat_take_drop n) => s12_uniq. by rewrite (subenv_drop e12) (uniq_catRL s12_uniq) ?x_p2 // mem_cat x_p2. Qed.
imports: mathcomp(all_ssreflect) bigmin extra