proposition: Lemma domeq_eta (K : ordType) (C : pred K) (U : union_map_class C unit) (f1 f2 : U) : dom_eq f1 f2 -> f1 = f2.
proof: Proof. case/domeqP=>V E; case V1 : (valid f1); last first. - by move: V1 (V1); rewrite {1}V; do 2![move/negbT/invalidE=>->]. apply: find_eta=>//; first by rewrite -V. move=>k; case D : (k \in dom f1); move: D (D); rewrite {1}E. - by do 2![case: dom_find=>// [[-> _]]]. by do 2![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)