Coqで証明　述語論理　スコープに関する命題

述語論理において変数のスコープは重要です。
というか数学やプログラミング全体で変数のスコープは重要でしょう。
以下はスコープの操作に関する命題です。
Parameterコマンドで共通に使うためのグローバル変数を定義しています。

Require Import Utf8 Classical.

Parameter U:Type.

Parameter P Q:U→Prop.

Goal (∀x,P x)∧(∀x,Q x)↔(∀x,P x∧Q x).
Proof.
split.
intro.
case H.
split.
eapply H0.
eapply H1.
split.
intro.
eapply H.
eapply H.
Qed.

Goal (∃x,P x)∨(∃x,Q x)↔(∃x,P x∨Q x).
Proof.
split.
intro.
destruct H,H.
exists x.
left.
assumption.
exists x.
right.
assumption.
intro.
destruct H,H.
left.
exists x.
assumption.
right.
exists x.
assumption.
Qed.

Goal (∀x,P x)∨(∀x,Q x)↔(∀x y,P x∨Q y).
Proof.
split.
intros.
case H.
left.
eapply H0.
right.
eapply H0.
intro.
apply NNPP.
intro.
apply H0.
left.
intro.
apply NNPP.
contradict H0.
right.
intro.
destruct(H x x0).
contradiction.
assumption.
Qed.

Goal (∃x,P x)∧(∃x,Q x)↔(∃x y,P x∧Q y).
Proof.
split.
intro.
destruct H,H,H0.
exists x,x0.
split.
assumption.
assumption.
intro.
destruct H,H,H.
split.
exists x.
assumption.
exists x0.
assumption.
Qed.