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