proposition: Lemma new_whites e1 e2 : wf_env e2 -> subenv e1 e2 -> whites e1 :\: whites e2 = blacks e2 :\: blacks e1.
proof: Proof. move=> e2_wf e12; rewrite whitesE -(subenv_grays e12) setDE setCK setIC -setDE. rewrite setDUl setDE setCU setIA setICr set0I set0U. rewrite setDUr (setIidPr _) // [_ :\: grays _](setDidPl _) ?subsetDl //. by apply/pred0P => y /=; case: colorP. Qed.
imports: mathcomp(all_ssreflect) bigmin extra