proposition: Lemma umpleq_some x1 x2 t s : valid x2 -> [pcm x1 <= x2] -> find t x1 = Some s -> find t x2 = Some s.
proof: Proof. by move=>W H; case: H W=>a -> W H; rewrite findUnL // (find_some H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)