fact: Definition subenv e1 e2 := [&& grays e1 == grays e2, blacks e1 \subset blacks e2, esccs e1 \subset esccs e2 & [exists n : 'I_infty.+1, stack e1 == drop n (stack e2)]].
imports: mathcomp(all_ssreflect) bigmin extra