diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-04 19:26:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-04 19:26:40 +0000 |
| commit | 4bff00735ae3162fd1e244b022a35a5efe58912e (patch) | |
| tree | c0ce875ea4a4ac6d811dcdae83c098e49253431e /theories/Logic/Berardi.v | |
| parent | ff949bd2a1f4ca4e1428e2ed96c9e46cc0d14cca (diff) | |
Petite simplification en passant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8122 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Berardi.v')
| -rw-r--r-- | theories/Logic/Berardi.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index f612e92d2..27e375f62 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. |