proposition: Lemma new_seenE e1 e2 : wf_env e1 -> wf_env e2 -> subenv e1 e2 -> (new_seen e1 e2) = (new_stack e1 e2) :|: cover (esccs e2) :\: cover (esccs e1).
proof: Proof. move=> e1_wf e2_wf sube12; rewrite !seenE//; apply/setP=> x. rewrite !inE -!num_sccs -?num_lt_V//; do 2!case: ltngtP => //=. by rewrite num_lt_V// (sub_num_lt sube12)// => ->; rewrite ltnNge max_card. by move=> xe2 xe1; move: xe2; rewrite (sub_snum sube12)// ?xe1// ltnn. Qed.
imports: mathcomp(all_ssreflect) bigmin extra