proposition: Lemma subenv_trans e2 e1 e3 : wf_color e2 -> wf_color e3 -> subenv e1 e2 -> subenv e2 e3 -> subenv e1 e3.
proof: Proof. move=> e2_wf e3_wf e12 e23; rewrite /subenv. rewrite (subenv_gray e23) (subenv_gray e12) eqxx. rewrite (subset_trans (subenv_black e12)) ?subenv_black //. rewrite (subset_trans (subenv_sccs e12)) ?subenv_sccs //=. apply/andP; split. apply/forall_inP=> x xIse1; apply/eqP. rewrite -(subenv_num e12) // (subenv_num e23) //. by case: (subenv_stackP e2_wf e12) => l -> _; rewrite mem_cat xIse1 orbT. apply/'exists_eqP; apply: uniq_ex_drop; first exact: wf_uniq. case: (subenv_stackP _ e23) => // s2 -> _. case: (subenv_stackP _ e12) => // s1 -> _. by exists (s2 ++ s1); rewrite catA. Qed.
imports: mathcomp(all_ssreflect) bigmin extra