proposition: Theorem exlist_ok : forall (A : Set) (P : A -> Prop) (qlist : list A), exlist A P qlist <-> (exists q : A, inlist A q qlist /\ P q).
proof: Proof. split. elim qlist. unfold inlist in |- *. simpl in |- *. intros. elim H. unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H. intro. split with q. split. left. reflexivity. assumption. intro. elim IH. intros q1 Hq1. elim Hq1. intros. split with q1. split. right. assumption. assumption. assumption. elim qlist. unfold inlist in |- *. simpl in |- *. intros. elim H. intros. elim H0. intros. elim H1. unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H. intros q1 Hq1. elim Hq1. intros. elim H0. intro. left. rewrite <- H2. assumption. intro. right. apply IH. split with q1. split. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ