fact: Definition dom_eq f1 f2 := match f1, f2 with Def fs1 _, Def fs2 _ => supp fs1 == supp fs2 | Undef, Undef => true | _, _ => false end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)