proposition: Lemma umall2_umfilt_oleq f1 f2 t : um_all2 (um_filter (fun kv => oleq kv.1 t) f1) (um_filter (fun kv => oleq kv.1 t) f2) <-> forall k, oleq k t -> optionR P (find k f1) (find k f2).
proof: Proof. split=>[H k X|H k]; last first. - move: (H k); rewrite !find_umfilt. case: (find k f1)=>[a1|]; case: (find k f2)=>[a2|] //=; by case: ifP=>// X; apply. move/umall2_umfilt_inv/(_ k): H=>/=. case: (find k f1)=>[v1|]; case: (find k f2)=>[v2|] //=. - by rewrite X; apply. - by rewrite X. by rewrite X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)