proposition: Lemma supp_eq_ins (s1 s2 : fmap) k1 k2 v1 v2 : path ord k1 (supp s1) -> path ord k2 (supp s2) -> supp (ins k1 v1 s1) =i supp (ins k2 v2 s2) -> k1 = k2 /\ supp s1 =i supp s2.
proof: Proof. move=>H1 H2 H; move: (H k1) (H k2). rewrite !supp_ins !inE /= !eq_refl (eq_sym k2). case: totalP=>/= E; last 1 first. - by move: H1; move/(ord_path E); move/notin_path; move/negbTE=>->. - by move: H2; move/(ord_path E); move/notin_path; move/negbTE=>->. rewrite (eqP E) in H1 H2 H * => _ _; split=>// x; move: (H x). rewrite !supp_ins !inE /=; case: eqP=>//= -> _. by rewrite (negbTE (notin_path H1)) (negbTE (notin_path H2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)