proposition: Lemma nexts_valid ps s1 : valid_pair ps -> valid_state s1 -> valid_pair (nexts ps s1).
proof: Proof. unfold nexts; match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => filters ps (f s1)) end. generalize ps s1 (movel_valid); elim movel; auto; clear ps s1. intros f lf Hrec ps s1 Hf Hg1 Hg; rewrite fold_left_cons. apply Hrec; auto with datatypes. generalize (filters_valid ps (f s1) Hg1); auto with datatypes. Qed.
imports: ZArith List