From 1f77a10f41e07324fd3df3676d68e005dd311e1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Nov 2003 22:57:14 +0000
Subject: Rien de bien important

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Hurkens.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 74629fccad..44d2594312 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -45,6 +45,7 @@ Definition I : U->Prop :=
   [x]((i:U->bool)(b2p (le i x))->(b2p (i [v](sb v U le x))))->B.
 
 Lemma Omega : (i:U->bool)(induct i)->(b2p (i WF)).
+Proof.
 Intros i y.
 Apply y.
 Unfold le WF induct.
@@ -54,7 +55,8 @@ Apply y.
 Exact H0.
 Qed.
 
-Lemma lemma : (induct [u](p2b (I u))).
+Lemma lemma1 : (induct [u](p2b (I u))).
+Proof.
 Unfold induct.
 Intros x p.
 Apply (p2p2 (I x)).
@@ -65,14 +67,16 @@ Apply q with i:=[y:?](i [v:V](sb v U le y)).
 Qed.
 
 Lemma lemma2 : ((i:U->bool)(induct i)->(b2p (i WF)))->B.
+Proof.
 Intro x.
-Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma)).
+Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma1)).
 Intros i H0.
 Apply (x [y](i [v](sb v U le y))).
 Apply (p2p1 ? H0).
 Qed.
 
-Lemma paradox : B.
+Theorem paradox : B.
+Proof.
 Exact (lemma2 Omega).
 Qed.
 
-- 
cgit v1.2.3