proposition: Lemma umall2_umfilt f1 f2 p : (forall k v1 v2, (k, v1) \In f1 -> (k, v2) \In f2 -> P v1 v2 -> p (k, v1) = p (k, v2)) -> um_all2 f1 f2 -> um_all2 (um_filter p f1) (um_filter p f2).
proof: Proof. move=>E H k; move: (H k); rewrite /optionR /= !find_umfilt. case E1: (find k f1)=>[v1|]; case E2: (find k f2)=>[v2|] // X. move/In_find: E1=>E1; move/In_find: E2=>E2. by rewrite -(E k v1 v2 E1 E2) //; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)