proposition: Lemma in_states_correct s ls : if in_states s ls then In s ls else ~In s ls.
proof: Proof. elim ls; simpl; auto. intros a l1 Hrec; generalize (state_eq_correct s a); case state_eq; auto. intros H1; generalize Hrec; case in_states; auto. intros HH [HH1 | HH1]; case H1; auto; case HH; auto. Qed.
imports: ZArith List