The Coq mailing list

[jean-francois.monin AT imag.fr]

You can adapt Laurent's solution to the dependent version.
It is better to use a reducible definition of less_or_equal
(no arith, no inversion, etc.): 

Fixpoint LE (n m:nat) {struct n} : Prop :=
  match n, m with
  | O, _ => True
  | (S n), O => False
  | (S n), (S m) => LE n m
  end.


Definition take3 :
   forall (x:list nat) (n: {i: nat | LE i (length x)}), list nat.
fix 1. 
intros l ([| i], H). 
  exact nil.
  destruct l as [|h t]; simpl in * |-*.
    case H.
    apply (cons h). apply (take3 t). exists i; exact H.
Defined.


Or even: 


Definition take4 : forall (l:list nat) (n:nat), LE n (length l) -> list nat.
fix 1. 
intros l [| n]. 
  intros _; exact nil.
  destruct l as [|h t]; simpl; intro H. 
    case H.
    exact (h :: take4 t n H).
Defined.


Hope this helps,
  JF

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 40