proposition: Lemma subset_seqL (T : finType) (A : pred T) (s : seq T) : (s \subset A) = ([set x in s] \subset A).
proof: Proof. by rewrite (eq_subset (in_set_seq _)). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)