From 864d5dfa689b4b2b59b85a3916832d43dbb1738b Mon Sep 17 00:00:00 2001 From: werner Date: Wed, 17 Apr 2002 14:49:35 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2656 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Lists/PolyList.v | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 817d06ce2..cd56ba1de 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -437,22 +437,19 @@ Definition nth_default : A -> list -> nat -> A := Lemma nth_In : (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l). -Proof. - Intros n l d. - Generalize n; Clear n. - NewInduction l. - Inversion 1. - Simpl. - NewInduction n. - Auto. - Right;Auto with arith. +Proof. +Unfold lt; Induction n ; Simpl. +Induction l ; Simpl ; [ Inversion 2 | Auto]. +Clear n ; Intros n hn ; Induction l ; Simpl. +Inversion 2. +Clear l ; Intros a l hl d ie ; Right ; Apply hn ; Auto with arith. Qed. - (********************************) (** Decidable equality on lists *) (********************************) + Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}. Proof. Induction x; NewDestruct y; Intros; Auto. -- cgit v1.2.3