proposition: Lemma candidate_valid l : (forall s, In s l -> valid_state s) -> (forall s, In s (candidate_list l) -> valid_state s).
proof: Proof. elim l; unfold candidate_list; auto; clear l. intros a l Hrec Hg s; rewrite fold_right_cons; intros H1. case (in_app_or _ _ _ H1); intros H2; auto with datatypes. assert (F0: valid_state a); auto with datatypes. rewrite in_map_iff in H2. case H2; intros f (Hf, Hf1); subst s. apply movel_valid; auto. Qed.
imports: ZArith List