proposition: Lemma codom_Some (T : finType) (s : seq (option T)) : None \notin s -> {subset s <= codom Some}.
proof: Proof. move => A [a|] B; by [rewrite codom_f|contrab]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)