proposition: Lemma make_conj_in : forall (A : Type) (eval : A -> Prop) (l : list A), make_conj eval l -> (forall p, In p l -> eval p).
proof: Proof. intros A eval l; induction l as [|? l IHl]. - simpl. tauto. - simpl. intros H ? H0. destruct l. + simpl in H0. destruct H0. * subst; auto. * tauto. + destruct H. destruct H0. * subst;auto. * apply IHl; auto. Qed.
imports: List