proposition: Lemma fmap_ind' (P : fmap -> Prop) : P nil -> (forall k v s, path ord k (supp s) -> P s -> P (ins k v s)) -> forall s, P s.
proof: Proof. move=>H1 H2; case; elim=>[|[k v] s IH] /= H. - by rewrite (_ : FinMap _ = nil); last by rewrite fmapE. have S: sorted ord (map key s) by apply: path_sorted H. rewrite (_ : FinMap _ = ins k v (FinMap S)); last by rewrite fmapE /= last_ins'. by apply: H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)