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