proposition: Lemma nexts_incl ps s : incl (snd ps) (fst ps) -> incl (snd (nexts ps s)) (fst (nexts ps s)).
proof: Proof. destruct ps as (ss1, ss2); unfold nexts; match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => filters ps (f s)) end. generalize ss1 ss2 s; elim movel; auto; clear ss1 ss2 s. intros f lf Hrec ss1 ss2 s Hs; repeat rewrite fold_left_cons. generalize (filters_incl (ss1, ss2) (f s)). case filters; intros ss3 ss4 Hss3. apply Hrec; auto with datatypes. Qed.
imports: ZArith List