proposition: Lemma fmap_ind'' (P : fmap -> Prop) : P nil -> (forall k v s, (forall x, x \in supp s -> ord x k) -> P s -> P (ins k v s)) -> forall s, P s.
proof: Proof. move=>H1 H2; case; elim/last_ind=>[|s [k v] IH] /= H. - by rewrite (_ : FinMap _ = nil); last by rewrite fmapE. have Sb: subseq (map key s) (map key (rcons s (k, v))). - by elim: s {IH H}=>[|x s IH] //=; rewrite eq_refl. have S : sorted ord (map key s). - by apply: subseq_sorted Sb H; apply: ordtype.trans. have T : forall x : K, x \in map key s -> ord x k. - elim: {IH Sb S} s H=>[|[k1 v1] s IH] //= L x. rewrite inE; case/orP; last by apply: IH; apply: path_sorted L. move/eqP=>->; elim: s {IH} L=>[|[x1 w1] s IH] /=; first by rewrite andbT. by case/andP=>O /(ord_path O) /IH. rewrite (_ : FinMap _ = ins k v (FinMap S)). - by apply: H2 (IH _)=>x /T. by rewrite fmapE /= first_ins'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)