proposition: Lemma In_U x k v f : x \In upd k v f <-> valid (upd k v f) /\ [\/ x.1 == k /\ x.2 = v | x.1 != k /\ x \In f].
proof: Proof. rewrite InU; split; case=>W H; split=>//. - by case: eqP H; [left | right]. by case: H=>[[->]//|[/negbTE ->]]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)