proposition: Lemma in_disj_kfilt p1 p2 s : {in supp s, forall x, ~~ p1 x || ~~ p2 x} -> disj (kfilter p1 s) (kfilter p2 s).
proof: Proof. elim/fmap_ind': s=>[|k v s _ IH] //= H. rewrite !kfilt_ins; case: ifP=>E1; case: ifP=>E2. - move: (H k); rewrite E1 E2 supp_ins inE /= eq_refl /=. by move/(_ (erefl _)). - rewrite disjC disj_ins disjC supp_kfilt mem_filter negb_and E2 /=. by apply: IH=>x S; apply: H; rewrite supp_ins inE /= S orbT. - rewrite disj_ins supp_kfilt mem_filter negb_and E1 /=. by apply: IH=>x S; apply: H; rewrite supp_ins inE /= S orbT. by apply: IH=>x S; apply: H; rewrite supp_ins inE /= S orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)