proposition: Lemma freePtUn2 k1 k2 v f : valid (pts k2 v \+ f) -> free (pts k2 v \+ f) k1 = if k1 == k2 then f else pts k2 v \+ free f k1.
proof: Proof. move=>V'; rewrite freeUn domPtUn inE V' /= eq_sym. rewrite ptsU freeU (validPtUn_cond V') free0. case: eqP=>/= E; first by rewrite E unitL (dom_free (validPtUnD V')). by case: ifP=>// N; rewrite dom_free // N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)