fact: Definition nexts (ps : states * states) s := fold_left (fun (ps : states * states) f => let (states, nstates) := ps in let s := f s in if in_states s states then ps else let states1 := s :: states in let nstates1 := s :: nstates in (states1, nstates1)) movel ps.
imports: ZArith List