proposition: Lemma pts_pf vars keys1 keys2 k v (f : xfind keys1 keys2 k): axiom (Context keys1 vars) (Context keys2 vars) [:: Pts k v] (key_tag (pts (xuntag f) v)).
proof: Proof. by case: f=>p [E H]; split=>//=; rewrite ?E ?unitR // (onth_size E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)