The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Hello,

Another alternative would be to use the Program extension and write:

Program Fixpoint SupL (n:nat) (f:Less n -> nat) {struct n} : nat :=
  match n with
    | 0 => 0
    | S n' => f n'
  end.

You can look at the definition of SupL to see how equalities between  
the matched term and the patterns are kept in each branch. They are  
used to discharge the proof obligation arising from the coercion of n'  
from nat to Less n at the "f n'" call. Program is documented in the  
manual.

--
Matthieu Sozeau
http://www.lri.fr/~sozeau