proposition: Lemma subenv_stack_gt e1 e2 x y : subenv e1 e2 -> wf_num e1 -> wf_color e1 -> wf_color e2 -> wf_num e2 -> x \in stack e1 -> y \in stack e2 -> y \notin stack e1 -> num e2 x < num e2 y.
proof: Proof. move=> sube12 e1_nwf e1_cwf e2_cwf e2_nwf x_stack1 y_stack2 yNstack1. case: (@subenv_stackP e1 e2) => // s s_def _. rewrite ltnNge wf_num_stack //; last first. by rewrite s_def mem_cat x_stack1 orbT. rewrite s_def !index_cat; have ys : y \in s. by have := y_stack2; rewrite s_def mem_cat (negPf yNstack1) orbF. rewrite ifN; last first. have := wf_uniq e2_cwf; rewrite s_def => /(@uniq_catRL _ x). by rewrite mem_cat x_stack1 orbT -s_def wf_uniq// => <-. by rewrite ifT// -ltnNge (@leq_trans (size s))// ?index_mem// leq_addr. Qed.
imports: mathcomp(all_ssreflect) bigmin extra