proposition: Lemma disj_kfilt p1 p2 s1 s2 : disj s1 s2 -> disj (kfilter p1 s1) (kfilter p2 s2).
proof: Proof. elim/fmap_ind': s2 s1=>[|k v s _ IH] s1 /=. - by rewrite kfilt_nil => _; case: disjP. rewrite disj_ins; case/andP=>H1 H2; rewrite kfilt_ins. case: ifP=>E; last by apply: IH. rewrite disj_ins supp_kfilt mem_filter negb_and H1 orbT /=. by apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)