proposition: Lemma cancel2 k1 k2 f1 f2 v1 v2 : valid (pts k1 v1 \+ f1) -> pts k1 v1 \+ f1 = pts k2 v2 \+ f2 -> if k1 == k2 then v1 = v2 /\ f1 = f2 else [/\ free f2 k1 = free f1 k2, f1 = pts k2 v2 \+ free f2 k1 & f2 = pts k1 v1 \+ free f1 k2].
proof: Proof. move=>V1 E; case: ifP=>X. - by rewrite -(eqP X) in E; case/(cancel V1): E. move: (V1); rewrite E => V2. have E' : f2 = pts k1 v1 \+ free f1 k2. - move: (erefl (free (pts k1 v1 \+ f1) k2)). rewrite {2}E freeUn E domPtUn inE V2 eq_refl /=. by rewrite ptsU freeU eq_sym X free0 -ptsU freePtUn. suff E'' : free f1 k2 = free f2 k1. - by rewrite -E''; rewrite E' joinCA in E; case/(cancel V1): E. move: (erefl (free f2 k1)). by rewrite {1}E' freePtUn // -E' (validE2 V2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)