proposition: Lemma fnd_ins k1 k2 v (s : fmap) : fnd k1 (ins k2 v s) = if k1 == k2 then Some v else fnd k1 s.
proof: Proof. case: s => s H; rewrite /fnd /=. elim: s k1 k2 v H=>[|[k' v'] s IH] //= k1 k2 v H. - by case: ifP=>H1; [rewrite (eqP H1) eq_refl | rewrite eq_sym H1]. case: ifP=>H1 /=. - by case: ifP=>H2; [rewrite (eqP H2) eq_refl | rewrite (eq_sym k1) H2]. case: ifP=>H2 /=. - rewrite (eqP H2). by case: ifP=>H3; [rewrite (eqP H3) eq_refl | rewrite eq_sym H3]. case: ifP=>H3; first by rewrite -(eqP H3) eq_sym H2. by apply: IH; apply: path_sorted H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)