One subtle difference between constraints and propositions is:

Suppose
    div1 : forall n m, m <> 0 -> nat

    div2 :: (n::nat) (m::nat) :: nat | m != 0

There is no way to typecheck
    div2 7 0

But, within a nonsensical branch you can obtain a proof of 0 <> 0:
    let f:False

    div1 7 0 (False_ind (0 <> 0) f)