fact: Fixpoint pprint i ts := if ts is t :: ts' then if ts' is [::] then interp' i t else interp' i t \+ pprint i ts' else Unit.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)