proposition: Lemma umall2_dom f1 f2 : um_all2 f1 f2 -> dom f1 = dom f2.
proof: Proof. move=>H; apply/domE=>k; apply/idP/idP; move: (H k); rewrite /optionR /=; by case: dom_find =>// v ->; case: dom_find=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)