proposition: Lemma next2s_valid p ps s : valid_triple ps -> valid_state s -> valid_triple (next2s p ps s).
proof: Proof. unfold next2s. match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => let s1 := f s in filter2s p ps s1) end. generalize ps s (movel_valid); elim movel; auto; clear ps s. intros f lf Hrec ps s1 Hf Hg1 Hg; rewrite fold_left_cons. apply Hrec; auto with datatypes. generalize (filter2s_valid p ps (f s1) Hg1); auto with datatypes. Qed.
imports: ZArith List