proposition: Lemma umapE (f g : base) : f = g <-> match f, g with Def f' pf, Def g' pg => f' = g' | Undef, Undef => true | _, _ => false end.
proof: Proof. split; first by move=>->; case: g. case: f; case: g=>// f pf g pg E; rewrite {g}E in pg *. by congr Def; apply: eq_irrelevance. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)