proposition: Lemma heapE (h1 h2 : heap) : h1 = h2 <-> match h1, h2 with Def f' pf, Def g' pg => f' = g' | Undef, Undef => true | _, _ => false end.
proof: Proof. split; first by move=>->; case: h2. case: h1; case: h2=>// f1 pf1 f2 pf2 E. rewrite {f2}E in pf1 pf2 *. by congr Def; apply: eq_irrelevance. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)