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)