Consider the intensional Martin-Löf type theory without axiom of choice or the law of excluded middle.
Let $A:U_0$ be a type and $B:A\to U_0$ be a function such that $\Sigma_{a:A}(B(a)\to 0)$is inhabited. Then $W_{a:A}B(a)$ is inhabited and so $(W_{a:A}B(a)\to 0)\to 0$ is inhabited. As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one term in normal form. What is that term?