proposition: Lemma sub_seen e1 e2 : subenv e1 e2 -> seen e1 \subset seen e2.
proof: Proof. move=> sube12; apply/subsetP=> x; rewrite !inE => x_seen1. by rewrite (sub_snum sube12)// inE. Qed.
imports: mathcomp(all_ssreflect) bigmin extra