proposition: Lemma eq_in_kfilter p1 p2 s : {in supp s, p1 =1 p2} -> kfilter p1 s = kfilter p2 s.
proof: Proof. move=>H; apply/fmapE; rewrite /= /kfilter'. case: s H; rewrite /supp /=; elim=>[|[k v] s IH] //=. move/path_sorted/IH=>{IH} H H1. have ->: p1 k = p2 k by apply: H1; rewrite inE /= eq_refl. by rewrite H // => x E; apply: H1; rewrite inE /= E orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)