(* Ouverture d’une section *)
Section CalculPredicats.
(* Définition de 2 domaines pour les prédicats *)
Variable A B : Type.

(* Formule du second ordre : Quantification des prédicats phi et psi *)
Theorem Thm_8 : forall (P Q : A -> Prop),
               (forall x1 : A, (P x1) /\ (Q x1))
            -> (forall x2 : A, (P x2)) /\ (forall x3 : A, (Q x3)).
intros.
split.
intro x2.
destruct (H x2).
exact H0.
intro x3.
destruct (H x3).
exact H1.
Qed.

(* Formule du second ordre : Quantification des prédicats phi et psi *)
Theorem Thm_9 : forall (P : A -> B -> Prop),
               (exists x1 : A, forall y1 : B, (P x1 y1))
            ->  forall y2 : B, exists x2 : A, (P x2 y2).
intros.
destruct H.
exists x.
generalize y2.
exact H.
Qed.


(* Formule du second ordre : Quantification des prédicats phi et psi *)
Theorem Thm_10 : forall (P Q : A -> Prop),
                (exists x1 : A, (P x1) -> (Q x1))
             -> (forall x2 : A, (P x2)) -> exists x3 : A, (Q x3).
intros.
destruct H.
exists x.
cut (P x).
exact H.
generalize x.
exact H0.
Qed.

End CalculPredicats.