diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-03 16:33:06 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-03 16:33:06 +0000 |
| commit | 24f78632d7ec81c3f2675168de7e0987d42685df (patch) | |
| tree | c7a419aa3bfe4eb68f9815bb9def56a137e094fa /theories/Lists | |
| parent | fc747e20bce6a3708162f29b781d5d1bc01d05fd (diff) | |
interversion de deux Elim dans In_dec pour que la fonction extraite soit efficace
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/PolyList.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 0a6d05956..40af3d16e 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -240,7 +240,8 @@ Lemma In_dec : ((x,y:A){x=y}+{~x=y}) -> (a:A)(l:list){(In a l)}+{~(In a l)}. Proof. Induction l. Right; Apply in_nil. - Intros; Elim H0; Simpl; Elim (H a0 a); Auto. + Intros; Elim (H a0 a); Simpl; Auto. + Elim H0; Simpl; Auto. Right; Unfold not; Intros [Hc1 | Hc2]; Auto. Save. |