proposition: Lemma make_conj_impl : forall (A : Type) (eval : A -> Prop) (l : list A) (g : Prop), (make_conj eval l -> g) <-> make_impl eval l g.
proof: Proof. intros A eval l; induction l as [|? l IHl]. - simpl. tauto. - simpl. intros g. destruct l. + simpl. tauto. + generalize (IHl g). tauto. Qed.
imports: List