fact: Structure partition (k r : heap) := Partition {heap_of :> tagged_heap; _ : partition_axiom k r heap_of}.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)