The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

S3 wrote:
> Theorem permutation_12 n r: permutation n r = permutation2 n r.
>    unfold permutation.
>    unfold permutation2.
>    destruct (leb r n) as [] _eqn.
> Error: The correctness of the conclusion relies on the body of b
>    

In situations like this, it is useful to break the operation of 
[destruct] into stages.  Your example fails in the very first stage.

To simulate that stage, run:
    generalize (leb r n).
This tactic just tries to replace all occurrences of the term with a 
fresh variable.  The error message reveals that the result is ill-typed, 
due to a use of [leb_complete], one of whose arguments is typed in terms 
of [leb].  Because you replace a use of [leb], that argument assumes an 
improper type.

The easiest solution I know is to run [generalize (leb_complete r n)] 
first.  Then your original strategy works.