Require Import NaturalDeduction.
Lemma L43a (A : Type) (P : A -> Prop) : ((forall x, P x) -> (forall y, P y)) /\ ((forall y, P y) -> (forall x, P x)).
Proof.
And_Intro.
Impl_Intro.
Forall_Intro.
Forall_Elim in H with y.
assumption.
Impl_Intro.
Forall_Intro.
Forall_Elim in H with x.
assumption.
Qed.
Lemma L43b (A : Type) (P : A -> Prop) : ((exists x, P x) -> (exists y, P y)) /\ ((exists y, P y) -> (exists x, P x)).
Proof.
And_Intro.
Impl_Intro.
Exists_Elim in H.
Exists_Intro with x.
assumption.
Impl_Intro.
Exists_Elim in H.
Exists_Intro with x.
assumption.
Qed.
Lemma L65a (A : Type) (P : A -> A -> Prop) : ((forall x y, P x y) -> (forall y x, P x y)) /\ ((forall y x, P x y) -> (forall x y, P x y)).
Proof.
And_Intro.
Impl_Intro.
Forall_Intro.
Forall_Intro.
Forall_Elim in H with x.
Forall_Elim in H0 with y.
assumption.
Impl_Intro.
Forall_Intro.
Forall_Intro.
Forall_Elim in H with y.
Forall_Elim in H0 with x.
assumption.
Qed.
Lemma L65b (A : Type) (P : A -> A -> Prop) : ((exists x y, P x y) -> (exists y x, P x y)) /\ ((exists y x, P x y) -> (exists x y, P x y)).
Proof.
And_Intro.
Impl_Intro.
Exists_Elim in H.
Exists_Elim in H0.
Exists_Intro with x0.
Exists_Intro with x.
assumption.
Impl_Intro.
Exists_Elim in H.
Exists_Elim in H0.
Exists_Intro with x0.
Exists_Intro with x.
assumption.
Qed.
Lemma L65c (A : Type) (P : A -> Prop) : (~(forall x, P x) -> (exists x, ~P x)) /\ ((exists x, ~P x) -> ~(forall x, P x)).
Proof.
And_Intro.
Impl_Intro.
PBC.
assume (forall x : A, P x).
Not_Elim in H and H1.
assumption.
Forall_Intro.
PBC.
assume (exists x : A, ~ P x).
Not_Elim in H0 and H2.
assumption.
Exists_Intro with x.
assumption.
Impl_Intro.
Not_Intro.
Exists_Elim in H.
Forall_Elim in H0 with x.
Not_Elim in H1 and H2.
assumption.
Qed.
Lemma L65d (A : Type) (P : A -> Prop) : (~(exists x, P x) -> (forall x, ~P x)) /\ ((forall x, ~P x) -> ~(exists x, P x)).
Proof.
And_Intro.
Impl_Intro.
Forall_Intro.
Not_Intro.
assume (exists x : A, P x).
Not_Elim in H and H1.
assumption.
Exists_Intro with x.
assumption.
Impl_Intro.
Not_Intro.
Exists_Elim in H0.
Forall_Elim in H with x.
Not_Elim in H2 and H1.
assumption.
Qed.
Lemma L65f (A : Type) (P Q : A -> Prop) : ((forall x, P x /\ Q x) -> (forall x, P x) /\ (forall x, Q x)) /\ ((forall x, P x) /\ (forall x, Q x) -> (forall x, P x /\ Q x)).
Proof.
And_Intro.
Impl_Intro.
And_Intro.
Forall_Intro.
Forall_Elim in H with x.
And_Elim_1 in H0.
assumption.
Forall_Intro.
Forall_Elim in H with x.
And_Elim_2 in H0.
assumption.
Impl_Intro.
Forall_Intro.
And_Intro.
And_Elim_1 in H.
Forall_Elim in H0 with x.
assumption.
And_Elim_2 in H.
Forall_Elim in H0 with x.
assumption.
Qed.