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