proposition: Lemma domeq_sym f1 f2 : dom_eq f1 f2 = dom_eq f2 f1.
proof: Proof. suff L f f' : dom_eq f f' -> dom_eq f' f by apply/idP/idP; apply: L. by case/domeqP=>H1 H2; apply/domeqP; split. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)