proposition: Lemma keyP i n k ts : has (key n) ts -> onth (keyx i) n = Some k -> exists v, interp i ts = pts k v \+ interp i (kfree n ts).
proof: Proof. elim: ts=>[|t ts IH] //=; case: ifP=>[|_ H]. - by case: t=>//= _ v /eqP <- _ ->; exists v. by case/(IH H)=>v ->; exists v; rewrite joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)