proposition: Lemma interp_cons i e t : interp i (e :: t) = einterp i e :+ interp i t.
proof: Proof. by case:t=>//; rewrite unh0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)