Need alternative proof to $ \exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t $ I tried to prove 
$ \exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t $
as;


*

*$ \exists x (k(x) \rightarrow t)$

*$ \exists x (\neg k(x) \lor t)$

*$ \exists x (\neg k(x)) \lor \exists x(t)$

*$ \neg \forall x (k(x)) \lor \exists x(t)$

*$ \neg \forall x (k(x)) \lor t$

*$ \forall x (k(x)) \rightarrow t$
Also tried elimination and introduction on $ \forall$ and $ \exists$ operators, but couldn't find a smarter way out. I guess there should be a much more simpler way, any ideas? 

We assume that : $x$ is not free in $t$.
Thus : 

$∃x(k(x)→t)$ --- premise 

1) $k(x)→t$ --- assumed [a] for $\exists$E
2) $∀xk(x)$ --- assumed [b]
3) $k(x)$ --- from 2) by $\forall$E
4) $t$ --- from 1) and 3) by $\rightarrow$E
5)  $∀xk(x) \rightarrow t$ --- from 2) and 4) by $\rightarrow$I, discharging assumption [b]
We have derived  $∀xk(x) \rightarrow t$ from assumption [a] : $k(x)→t$. Due to the fact that $x$ is not free in $t$, we have that $x$ is not free in $∀xk(x) \rightarrow t$; thus the proviso for $\exists$E is fulfilled and we can derive :
6) $∀xk(x) \rightarrow t$ --- from 1) and 5) by $\exists$E, discharging assumption [a].
Thus, we have proved :


$∃x(k(x)→t) \vdash ∀xk(x) \rightarrow t$.


