diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:57:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:57:14 +0000 |
| commit | 1f77a10f41e07324fd3df3676d68e005dd311e1b (patch) | |
| tree | 390f48be1f057aa5a4b9752284f8d38ee59d3ec7 /theories/Logic/Hurkens.v | |
| parent | 34d8b72d72c11f74f1eef9b693c259903057e9d4 (diff) | |
Rien de bien important
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Hurkens.v')
| -rw-r--r-- | theories/Logic/Hurkens.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 74629fcca..44d259431 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. |