proposition: Lemma validUnEb f : valid (f \+ f) = unitb f.
proof: Proof. case E: (unitb f); first by move/unitbE: E=>->; rewrite unitL valid_unit. case: validUn=>// V' _ L; case: validEb E=>//; case; split=>// k. by case E: (k \in dom f)=>//; move: (L k E); rewrite E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)