proposition: Lemma fE i ts x : foldr (fx i) x ts = x \+ interp i ts.
proof: Proof. by elim: ts x=>[|t ts IH] x /=; rewrite ?unitR // IH /= joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)