fact: Definition eq_ptr (x y : ptr) : bool := match x, y with ptr_nat m, ptr_nat n => m == n end.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)