Rice's theorem in type theory From the formula
$$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$
we can get the scheme
$$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\neg\phi(x)$$
From the scheme
$$\forall x\colon A\,\exists y\colon A\,\phi(x,y)\Rightarrow\exists x\colon A\,\phi(x,x)$$
we can get 
$$\forall x\colon A\,(\phi(x)\vee\psi(x))\Rightarrow\neg\neg(\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\psi(x))$$
Where can I find these results? Give me a link, please.
P.S. Sorry, the second scheme must be
$$\forall x\colon A\,(\neg\phi(x)\vee\neg\psi(x))\Rightarrow\neg\neg(\forall x\colon A\,\neg\phi(x)\vee\forall x\colon A\,\neg\psi(x))$$
The results are not quite difficult, but I never saw it in articles or books.
 A: I'll prove the first scheme; you can find a link by using the cite button below this answer.
First, we show that $$\forall x,y : A\,(\phi(x) \lor \lnot\phi(y))\tag{*}\label{eq}.$$ To see this, given $x,y : A$, define the function $$f_{x,y}(z) = \begin{cases} x & \text{if $\phi(z)$,} \\ y &\text{if $\lnot\phi(z)$.} \end{cases}$$ By hypothesis, $f_{x,y}$ has must have a fixed point. Since $$\forall z: A\,(f_{x,y}(z) = x \lor f_{x,y}(z) = y)$$ that fixed point must either be $x$ or $y$. Thus $$\forall x, y: A\,(f_{x,y}(x) = x \lor f_{x,y}(y) = y).$$ If $f_{x,y}(x) = x$ then $\phi(x)$ and if $f_{x,y}(y) = y$ then $\lnot\phi(y)$, so we conclude that \eqref{eq} is indeed true.
This is almost what we need. For the final stretch, first note that $A$ is inhabited since the identity function must have a fixed point. So fix $z:A$. We know that $\phi(z) \lor \lnot\phi(z)$. If $\phi(z)$ then $\phi(x) \lor \lnot\phi(z)$ is equivalent to $\phi(x)$ for any $x:A$, and so the instance of \eqref{eq} with $y = z$ gives $\forall x: A\,\phi(x)$. If $\lnot\phi(z)$ then $\phi(z) \lor \lnot\phi(y)$ is equivalent to $\lnot\phi(y)$ for any $y:A$, and so the instance of \eqref{eq} with $x = z$ gives $\forall y:A\,\lnot\phi(y).$ Thus, we conclude that $$\forall x:A\,\phi(x) \lor \forall y:A\,\lnot\phi(y),$$ which is an alphabetic variant of your desired conclusion.
