proposition: Lemma seen_store (A : {set V}) e : A \subset seen e -> seen (store A e) = seen e.
proof: Proof. move=> A_sub; apply/setP=> x; rewrite !inE/= ffunE. by case: ifPn => // /(subsetP A_sub); rewrite inE leqnn => ->. Qed.
imports: mathcomp(all_ssreflect) bigmin extra