proposition: Lemma forall_all (T : finType) (p : {pred T}) : [forall x, p x] = all p (enum T).
proof: Proof. apply/forallP/allP => [|H x]; by [firstorder|apply/H/mem_enum]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)