proposition: Lemma interp_rev i ts : interp i (rev ts) = interp i ts.
proof: Proof. elim: ts=>[|t ts IH] //=; rewrite rev_cons -cats1. by rewrite /interp foldr_cat fE /= unitR IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)