diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/PolyList.v | 17 |
1 files 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. |