proposition: Lemma seqof_ins k v (s : fmap) : path ord k (supp s) -> seq_of (ins k v s) = (k, v) :: seq_of s.
proof: Proof. by case: s; elim=>[|[k1 v1] s IH] //= _; case/andP=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)