proposition: Lemma valid_cons i e t : valid i (e :: t) = valid i [:: e] && valid i t.
proof: Proof. case: e=>[x d|v] /=; rewrite /valid /=; by [rewrite !andbT andbA | rewrite andbT andbCA]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)