proposition: Lemma ForallE (T : eqType) (P : T -> Prop) (s : list T) : List.Forall P s <-> (forall x, x \in s -> P x).
proof: Proof. split. - elim => //= {s} x s Px _ H. exact/all_cons. - elim: s => // x s IH /all_cons [Px Ps]. by constructor; auto. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)