  We show that call-by-need is observationally equivalent to weak-head needed
reduction. The proof of this result uses a semantical argument based on a
(non-idempotent) intersection type system called $\mathcal{V}$. Interestingly,
system $\mathcal{V}$ also allows to syntactically identify all the weak-head
needed redexes of a term.
