fact: Structure uform (k : heap) r := UForm {heap_ofU :> tagged_heapU; _ : uform_axiom k r heap_ofU}.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)