proposition: Lemma expP i n ts : has (exp n) ts -> interp i ts = onth (expx i) n \+ interp i (efree n ts).
proof: Proof. elim: ts=>[|t ts IH] //=; case: ifP=>/= [|_ H]. - by case: t=>/= m /eqP->. by rewrite (IH H) joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)