proposition: Lemma cons_subset (T : eqType) (a:T) s1 (s2 : pred T) : {subset a::s1 <= s2} <-> a \in s2 /\ {subset s1 <= s2}.
proof: Proof. exact: all_cons. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)