The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

frank maltman wrote:
> Definition fin_bound {b : nat} (_ : fin b) : nat := b.
>    

By the way, this function seems a bit non-idiomatic.  It's an identity 
function, and your proofs below would be simplified by referring 
directly to an index instead of to an identity function called on it.  
For instance, [simpl] would have exactly the behavior you want, with no 
need to use [unfold].

How much would the proof be simplified, you ask?  Let's see. ;)

Theorem lt_fin_nat_fb_b : forall (b : nat) (f : fin b),
  fin_nat f < b.
  induction f; crush.
Qed.