fact: Fixpoint interp i t := if t is e :: t' then if t' is [::] then einterp i e else einterp i e :+ interp i t' else empty.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)