proposition: Lemma cancel_ins k v (s1 s2 : fmap) : k \notin (supp s1) -> k \notin (supp s2) -> ins k v s1 = ins k v s2 -> s1 = s2.
proof: Proof. move: s1 s2=>[s1 p1][s2 p2]; rewrite !fmapE /supp /= {p1 p2}. elim: s1 k v s2=>[k v s2| [k1 v1] s1 IH1 k v s2] /=. - case: s2=>[| [k2 v2] s2] //= _. rewrite inE negb_or; case/andP=>H1 _; case: ifP=>// _. by rewrite (negbTE H1); case=>E; rewrite E eq_refl in H1. rewrite inE negb_or; case/andP=>H1 H2 H3. case: ifP=>H4; case: s2 H3=>[| [k2 v2] s2] //=. - rewrite inE negb_or; case/andP=>H5 H6. case: ifP=>H7; first by case=>->->->. by rewrite (negbTE H5); case=>E; rewrite E eq_refl in H5. - by rewrite (negbTE H1)=>_; case=>E; rewrite E eq_refl in H1. rewrite inE negb_or (negbTE H1); case/andP=>H5 H6. rewrite (negbTE H5); case: ifP=>H7 /=. - by case=>E; rewrite E eq_refl in H1. by case=>->-> H; congr (_ :: _); apply: IH1 H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)