proposition: Lemma first_ins' (k : K) (v : V) s : (forall x, x \in map key s -> ord x k) -> ins' k v s = rcons s (k, v).
proof: Proof. elim: s=>[|[k1 v1] s IH] H //=. move: (H k1); rewrite inE eq_refl; move/(_ (erefl _)). case: ordP=>// O _; rewrite IH //. by move=>x H'; apply: H; rewrite inE /= H' orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)