proposition: Lemma uvalidL5 x y : uvalid (ujoin x y) -> uvalid x.
proof: Proof. by rewrite /uvalid; case/and5P; do ![move/validL=>->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)