proposition: Lemma pp_interp i ts : pprint i ts = interp i ts.
proof: Proof. by elim: ts=>[|t ts /= <-] //; case: ts=>//; rewrite unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)