proposition: Lemma umall2_umfilt_inv f1 f2 p : um_all2 (um_filter p f1) (um_filter p f2) -> forall k, match find k f1, find k f2 with Some v1, Some v2 => p (k, v1) && p (k, v2) -> P v1 v2 | Some v1, None => ~~ p (k, v1) | None, Some v2 => ~~ p (k, v2) | None, None => True end.
proof: Proof. move=>H k; move: (H k); rewrite !find_umfilt. case: (find k f1)=>[a1|]; case: (find k f2)=>[a2|] //. - by case: ifP; case: ifP. - by case: ifP. by case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)