(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch L05 (General Predicate Logic) The material in this file contains coq proofs which can be read and animated with coqide or xemacs+proofgeneral. **) Section l05. Section tautologies. Variable D : Set. Variables P Q: D -> Prop. Lemma AndAll : (forall x:D,P x) /\ (forall y:D,Q y) <-> forall z:D,P z /\ Q z. split. intros H d. destruct H as [HP HQ]. split. apply HP. apply HQ. intro H. split. intro d. cut (P d /\ Q d). intro HPQ. destruct HPQ as [HP HQ]. exact HP. apply H. intro d. cut (P d /\ Q d). intro HPQ. destruct HPQ as [HP HQ]. exact HQ. apply H. Qed.