proposition: Lemma upd_eta k v f : upd k v f = pts k v \+ free f k.
proof: Proof. case W : (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite upd_undef free_undef join_undef. case H : (C k); last first. - by move/negbT: H=>H; rewrite (upd_condN v) // pts_condN // undef_join. have W' : valid (pts k v \+ free f k). - by rewrite validPtUn H validF W domF inE eq_refl. apply: find_eta=>//; first by rewrite validU H W. by move=>k'; rewrite findU H W findPtUn2 // findF; case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)