proposition: Lemma unguard_pts_pf A k (v : A) : unguard_ax (PtOmf k v) (pt_tag (pts k v)).
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)