proposition: Lemma varP i n u ts : has (var n) ts -> onth (varx i) n = Some u -> interp i ts = u \+ interp i (vfree n ts).
proof: Proof. elim: ts=>[|t ts IH] //=; case: ifP=>[|_ H]. - by case: t=>//= _ /eqP <- _ ->. by move/(IH H)=>->; rewrite joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)