proposition: Lemma fmapE (s1 s2 : fmap) : s1 = s2 <-> seq_of s1 = seq_of s2.
proof: Proof. split=>[->|] //. move: s1 s2 => [s1 H1] [s2 H2] /= H. by rewrite H in H1 H2 *; rewrite (bool_irrelevance H1 H2). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)