diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
| commit | 3675bac6c38e0a26516e434be08bc100865b339b (patch) | |
| tree | 87f8eb1905c7b508dea60b1e216f79120e9e772d /theories/Logic/Classical_Pred_Type.v | |
| parent | c881bc37b91a201f7555ee021ccb74adb360d131 (diff) | |
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Classical_Pred_Type.v')
| -rwxr-xr-x | theories/Logic/Classical_Pred_Type.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 6bfd08e43..f3f29747c 100755 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -18,7 +18,7 @@ Variable U : Type. (** de Morgan laws for quantifiers *) Lemma not_all_ex_not : - forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U | ~ P n. + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. Proof. unfold not in |- *; intros P notall. apply NNPP; unfold not in |- *. @@ -30,7 +30,7 @@ apply abs; exists n; trivial. Qed. Lemma not_all_not_ex : - forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U | P n. + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. Proof. intros P H. elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. @@ -38,7 +38,7 @@ apply NNPP; trivial. Qed. Lemma not_ex_all_not : - forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n. + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. Proof. unfold not in |- *; intros P notex n abs. apply notex. @@ -46,7 +46,7 @@ exists n; trivial. Qed. Lemma not_ex_not_all : - forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n. + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. Proof. intros P H n. apply NNPP. @@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial. Qed. Lemma ex_not_not_all : - forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n). + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). Proof. unfold not in |- *; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : - forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n). + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). Proof. unfold not in |- *; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. |