proposition: Lemma AllS_x_P : forall A P l (x:A), AllS P l -> In x l -> P x.
proof: Proof. intros. induction H. simpl in H0. elim H0. elim H0. intro eq_a_x. rewrite <- eq_a_x; exact H. assumption. Qed.
imports: Coq(List) Coq(Arith)