proposition: Lemma fmapP (s1 s2 : fmap) : (forall k, fnd k s1 = fnd k s2) -> s1 = s2.
proof: Proof. rewrite /fnd; move: s1 s2 => [s1 P1][s2 P2] H; rewrite fmapE /=. elim: s1 P1 s2 P2 H=>[|[k v] s1 IH] /= P1. - by case=>[|[k2 v2] s2 P2] //=; move/(_ k2); rewrite eq_refl. have S1: sorted ord (map key s1) by apply: path_sorted P1. case=>[|[k2 v2] s2] /= P2; first by move/(_ k); rewrite eq_refl. have S2: sorted ord (map key s2) by apply: path_sorted P2. move: (IH S1 s2 S2)=>{IH} /= IH H. move: (notin_path P1) (notin_path P2)=>N1 N2. case E: (k == k2). - rewrite -{k2 E}(eqP E) in P2 H N2 *. move: (H k); rewrite eq_refl=>[[E2]]; rewrite -E2 {v2 E2} in H *. rewrite IH // => k'. case E: (k == k'); first by rewrite -(eqP E) !notin_filter. by move: (H k'); rewrite E. move: (H k); rewrite eq_refl eq_sym E notin_filter //. move: (total k k2); rewrite E /=; case/orP=>L1. - by apply: notin_path; apply: ord_path P2. move: (H k2); rewrite E eq_refl notin_filter //. by apply: notin_path; apply: ord_path P1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)