proposition: Lemma eq_in_pmap (aT : eqType) rT (f1 f2 : aT -> option rT) (s : seq aT) : {in s, f1 =1 f2} -> pmap f1 s = pmap f2 s.
proof: Proof. by elim: s => // a s IHs /all_cons [eq_a eq_s]; rewrite /= eq_a (IHs eq_s). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)