proposition: Lemma keyN i n ts : ~~ has (key n) ts -> interp i (kfree n ts) = interp i ts.
proof: Proof. by elim: ts=>[|t ts IH] //=; case: ifP=>//= _ /IH ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)