proposition: Lemma eval_cat i s1 s2 : eval i (s1 ++ s2) <-> eval i s1 /\ eval i s2.
proof: Proof. elim: s1=>[/=|f s1 IH]; first tauto. by rewrite cat_cons !eval_cons IH; tauto. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)