From 4bff00735ae3162fd1e244b022a35a5efe58912e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Mar 2006 19:26:40 +0000
Subject: Petite simplification en passant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/Berardi.v | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index f612e92d2a..27e375f629 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -92,14 +92,10 @@ End Retracts.
 Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
 Proof.
 intros A B.
-elim (EM (retract (pow A) (pow B))).
-intros [f0 g0 e].
-exists f0 g0.
-trivial.
-
-intros hf.
-exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F).
-intros; elim hf; auto.
+destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
+  exists f0 g0; trivial.
+  exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; 
+    destruct hf; auto.
 Qed.
 
 
-- 
cgit v1.2.3