proposition: Lemma last_ins' (x : K) (v : V) s : path ord x (map key s) -> ins' x v s = (x, v) :: s.
proof: Proof. by elim: s=>[|[k1 v1] s IH] //=; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)