proposition: Lemma eval_cons i f s : eval i (f :: s) <-> eval_fact i f /\ eval i s.
proof: Proof. by case:s=>//; split=>//; case. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)