proposition: Lemma um0PtE (k : K) (v : V) : (@Unit [pcm of union_map K V] == k \\-> v) = false.
proof: Proof. by rewrite eq_sym umPt0E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)