The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Daniel Schepler 
>>>>> <dschepler AT gmail.com>
>>>>>  writes:

> OK, here's a complete solution.  As opposed to what Auger suggested, my
> proof essentially proceeds by cases depending on whether or not FinO is in
> the list.  That makes it easier to define the injection { x:Fin (S n) | x <>
> FinO } -> Fin n.

Thank you, Daniel.  I'm using this lemma to prove properties about a much
bigger algorithm, so I very much appreciate your help in getting unstuck.

John