proposition: Lemma heap_base : null \notin supp f -> all (fun k => k != null) (supp f).
proof: Proof. by move=>H; apply/allP=>k; case: eqP H=>// -> /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)