proposition: Lemma domeq_trans f1 f2 f3 : dom_eq f1 f2 -> dom_eq f2 f3 -> dom_eq f1 f3.
proof: Proof. case/domeqP=>E1 H1 /domeqP [E2 H2]; apply/domeqP=>//. by split=>//; [rewrite E1 E2 | move=>x; rewrite H1 H2]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)