fact: Definition dom_eq h1 h2 := match h1, h2 with Def f1 _, Def f2 _ => supp f1 == supp f2 | Undef, Undef => true | _, _ => false end.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)