proposition: Lemma fold_nexts_valid ps ss : valid_pair ps -> (forall s, In s ss -> valid_state s) -> valid_pair (fold_left nexts (snd ps) (fst ps, ss)).
proof: Proof. destruct ps as (ss1, ss2); simpl fst; simpl snd. revert ss1 ss; elim ss2; clear ss2; auto. - simpl; intros ss1 ss (HH, _) HH1; split; auto. - intros s ss2 Hrec ss1 ss Hg1 Hg; rewrite fold_left_cons. generalize (nexts_valid (ss1, ss) s); case nexts. intros ss3 ss4 Hg2. case Hg1; simpl fst; simpl snd; intros Hg3 Hg4; case Hg2; auto with datatypes. + split; auto. + simpl; intros Hg5 Hg6; apply Hrec; auto; split; auto. case Hg1; auto with datatypes. Qed.
imports: ZArith List