(** 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.