fact: Definition subenv e1 e2 := [&& gray e1 == gray e2, black e1 \subset black e2, esccs e1 \subset esccs e2, [forall x in stack e1, num e2 x == num e1 x] & [exists n : 'I_infty, stack e1 == drop n (stack e2)]].
imports: mathcomp(all_ssreflect) bigmin extra