proposition: Lemma candidate_in a l : In a (candidate_list l) <-> exists i, exists f, a = f i /\ In i l /\ In f movel.
proof: Proof. elim l; clear l. - split; intros H; case H; intros i (f, (_, (HH,_))); case HH. - intros b l Hrec; split. + intros H; case (in_app_or (map (fun y1 : state -> state => y1 b) movel) (candidate_list l) _ H). * elim movel; simpl; auto. -- intros HH; case HH. -- intros f lf Hrec1 [H1 | H1]. ++ exists b; exists f; auto. ++ case (Hrec1 H1); intros f1 (b1, (Hb1, (Hb2, Hb3))). exists f1; exists b1; auto. * rewrite Hrec; intros (i, (f, (Hb1, (Hb2, Hb3)))). exists i; exists f; auto with datatypes. + intros (i, (f, (Hf, (Hf1, Hf2)))); subst a. unfold candidate_list; rewrite fold_right_cons. match goal with |- context[fold_right ?X ?Y ?Z] => change (fold_right X Y Z) with (candidate_list Z) end. apply in_or_app. simpl in Hf1; case Hf1; clear Hf1; intros Hf1. * subst b; left; generalize Hf2; elim movel; simpl; auto. intros f1 lf Hrec1 [H1 | H1]; auto; subst f1; auto. * right; rewrite Hrec. exists i; exists f; auto. Qed.
imports: ZArith List