proposition: Theorem alllist_ok : forall (A : Set) (P : A -> Prop) (qlist : list A), alllist A P qlist <-> (forall q : A, inlist A q qlist -> P q).
proof: Proof. split. elim qlist. unfold inlist in |- *. simpl in |- *. intros. elim H0. unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H. intros. elim H2. intro. rewrite H3. assumption. intro. apply IH. assumption. assumption. elim qlist. unfold inlist in |- *. simpl in |- *. intros. trivial. unfold inlist in |- *. simpl in |- *. intros q l IH H. split. apply H. left. reflexivity. apply IH. intros. apply H. right. assumption. Qed.
imports: Arith ZArith EqNat dec natZ