proposition: Lemma eval_rcons i f s : eval i (rcons s f) <-> eval i s /\ eval_fact i f.
proof: Proof. by rewrite -cats1 eval_cat. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)