proposition: Lemma card_val (T : finType) (P : pred T) (s : subFinType P) (A : pred s) : #|val @: A| = #|A|.
proof: Proof. by rewrite card_imset. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)