What is the difference between the following types for the $head$ function on a vector of integers.
($head$ takes a natural number $n$ and a vector $v$ of length $n$ or $(n+1)$ (depending on the type), and returns the first element of the vector. The key premise here is that the input vector should be non-empty)
$\Pi n:nat. vector ~(n+1) \rightarrow int$
$\Pi n:nat. (n > 0) \rightarrow vector~n \rightarrow int$
The first type is along the lines of $first$ function in the ATAPL textbook by Pierce et.al. (page 46). However, I want to know the difference (from type checking perspective) w.r.t the second type which requires a proof that $(n > 0)$.
Does the second type mean that the language should support Proposition (similar to Coq)? Specifically, I am wondering if the second type is possible in a first order dependent typed language like $\lambda LF$ calculus that does not support any explicit propositions/proofs (Fig 2-1, page 51, Section 2.2 of ATAPL textbook).