proposition: Lemma feqP : Equality.axiom feq.
proof: Proof. move=>s1 s2; rewrite /feq. case: eqP; first by move/fmapE=>->; apply: ReflectT. by move=>H; apply: ReflectF; move/fmapE; move/H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)