proposition: Lemma umall2_find X f1 f2 (f : option V -> X) t : (forall k v1 v2, (k, v1) \In f1 -> (k, v2) \In f2 -> P v1 v2 -> f (Some v1) = f (Some v2)) -> um_all2 f1 f2 -> f (find t f1) = f (find t f2).
proof: Proof. move=>E /(_ t). case E1: (find t f1)=>[v1|]; case E2: (find t f2)=>[v2|] //=. by move/In_find: E1=>E1; move/In_find: E2=>E2; apply: E E1 E2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)