fact: Fixpoint eval i s := match s with | [:: f] => eval_fact i f | (f :: fs) => eval_fact i f /\ eval i fs | [::] => True end.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)