fact: Fixpoint execN (t : table) (n : nat) (s : State) : list State := match n with | O => [s] | S n' => match exec t s with | Some s' => s :: execN t n' s' | None => s :: nil end end%list.
imports: ZArith List MSetPositive