Demonstration Wick's theorem I read a lot about Wick's theorem, on the internet and on this site, but I'm unable to find the answer to my question.
I have a problem trying to demonstrate Wick's theorem: I know it is done by induction, so I had some issues with $k=2$, just the time to get used to sign swapping in normal and chronological ordering, in the case of fermionic field, but after that everything was cool.
Now, assuming it is right for generic $k$, I'm trying to demonstrate it for $k+1$. For what I understood everything starts from the fact that chronological ordering does not care about the original disposition of our field operators, so it seems legit to assume that our $\hat{\phi}_{k+1}$ is placed in an extremum of the line, suppose on the right one.
Well at this point I read everywere that I should decompose my field operator in the positive energies part $\hat{\phi}^+_{k+1}$, associated with particle annihilation and on the negative energies part, that is usually called $\hat{\phi}^-$, but that I call $\hat{\phi}^{-\dagger}_{k+1}$ because I'm extremely "error susceptible" (="dumb") and I need to remember that it is associated with the creation of an antiparticle.
Everything all right to me until here, I think.
This said it's easy to see that
$$
\,:\!
\overset{k}{\underset{i=1}{\circ}}
\hat{\phi}_i
\!:\,
\hat{\phi}_{k+1}^+
=
\,:\!
\overset{k}{\underset{i=1}{\circ}}
\hat{\phi}_i
\circ
\hat{\phi}_{k+1}^+
\,:\!
$$
because in normal ordering "nobody wants" an annihilation operator that was originally put in the right extremum of the line of operators, because normal ordering cares about original disposition.
But
What happens with the $\hat{\phi}_{k+1}^{-\dagger}$?
The problem is that I don't know what kind of fields I have so to be the most general possible I should put something like
$$
\hat{\phi}_i
\equiv
\hat{\phi}_i^+
+
\hat{\phi}_i^{-\dagger}
+
\hat{\phi}_i^{+\dagger}
+
\hat{\phi}_i^-
$$
and in this way normal ordering become an absolute mess!! Even with just two field operators is extremely difficult, so I can't find a way to explicit the normal ordering of all the field operators when I have to deal with
$$
\,:\!
\overset{k}{\underset{i=1}{\circ}}
\hat{\phi}_i
\!:\,
\hat{\phi}_{k+1}^{-\dagger}
=
??
$$
So my problem is how to express this quantity in terms of this other quantity, that is the one that I'm really interested on (clearly with all the contraction part that I'm not writing)
$$
\,:\!
\overset{k}{\underset{i=1}{\circ}}
\hat{\phi}_i
\hat{\phi}_{k+1}^{-\dagger}
\!:\,
$$
Thanks for everybody that can help me on this, even for just a little suggestion, because I'm really stuck and I don't know how to move.
 A: (Later edit, contains the proof of Wick's theorem)
As mentioned in the comments, due to the distributivity with respect to addition of the time-ordering, normal-ordering and contractions, proving Wick's theorem for field operators which generically can be decomposed intro a creation and annihilation part is equivalent to proving it for just those creation and annihilation terms. Thus, the aim is to prove (I'm switching now to your notation for normal ordering)
$$\mathcal{T}\{\prod_{i=1}^k\hat{F}_i\}=:\prod_{i=1}^k\hat{F}_i:+\,\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_k\}\tag{1}\label{wickfork}$$
where the normal-ordered sum of all possible contractions (a contraction is denoted by an arc over the contracted operators) is
$$\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_k\}=\sum_{j,l}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_l}:\prod_{i\neq j,l}^{1,k}\hat{F}_i:+\sum_{j,l}^{1,k}\sum_{m,n\neq j,l}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_l}\overset{\huge\frown}{\hat{F}_m\hat{F}_n}:\prod_{i\neq j,l,m,n}^{1,k}\hat{F}_i:+\dots$$
Notice that the contractions may be placed either inside or outside the normal product, since they are unaffected by it. Once this notation is introduced, it's time to proceed to the actual proof by induction. The result for $k=2$ is true by construction since
$$\mathcal{T}\{\hat{F}_1\hat{F_2}\}=:\hat{F}_1\hat{F}_2:+\overset{\huge\frown}{\hat{F}_1\hat{F}_2}$$
is just the definition for the contraction between two operators. Further, one assumes the result holds for a given $k$, expressed in \eqref{wickfork}. The aim is to prove this result for $k+1$, that is
$$\mathcal{T}\{\prod_{i=1}^{k+1}\hat{F}_i\}=:\prod_{i=1}^{k+1}\hat{F}_i:+\,\color{teal}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k+1}\}}\tag{2}\label{wickfork+1}$$
Simply multiplying \eqref{wickfork} to the right by $\hat{F}_{k+1}$ yields
$$\mathcal{T}\{\prod_{i=1}^k\hat{F}_i\}\hat{F}_{k+1}=:\prod_{i=1}^k\hat{F}_i:\hat{F}_{k+1}+\,\color{navy}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_k\}}\hat{F}_{k+1}\tag{3}\label{wickforktimesk+1}$$
The LHS of \eqref{wickfork+1} and \eqref{wickforktimesk+1} are equal, assuming $\hat{F}_{k+1}(t_{k+1})$ with $t_{k+1}<t_i$ where $i=\overline{1,k}$ from $\hat{F}_i(t_i)$. Hence
$$\mathcal{T}\{\prod_{i=1}^k\hat{F}_i\}\hat{F}_{k+1}=\mathcal{T}\{\prod_{i=1}^{k+1}\hat{F}_i\}$$
Therefore, we are left to prove that also the RHS of \eqref{wickfork+1} and \eqref{wickforktimesk+1} are the same. This is where Wick's lemma (proven in the original post below) becomes extremely useful. It states that multiplying a normal-ordered product to the right by another fermionic operator yields the normal product of all operators plus the normal-ordered sum of all operators in which the supplementary operator is contracted with every other operator
$$:\prod_{i=1}^k\hat{F}_i:\hat{F}_{k+1}=:\prod_{i=1}^{k+1}\hat{F}_i:+\color{purple}{\sum_{j}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}:\prod_{i\neq j}^{1,k}\hat{F}_i:}\tag{4}\label{generalizedwick0}$$
This may be generalized to the situation in which the normal product also contains a contraction within the set $\{\hat{F}_i\}_{i=\overline{1,k}}$
$$\color{navy}{\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq m,n}^{1,k}\hat{F}_i:}\hat{F}_{k+1}=\color{green}{\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq m,n}^{1,k}\hat{F}_i\,\hat{F}_{k+1}:}+\color{purple}{\sum_{j\neq m,n}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq j,m,n}^{1,k}\hat{F}_i:}\tag{5}\label{generalizedwick1}$$
and the same for two contractions
$$\color{navy}{\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq m,n,p,q}^{1,k}\hat{F}_i:}\hat{F}_{k+1}=\color{green}{\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq m,n,p,q}^{1,k}\hat{F}_i\,\hat{F}_{k+1}:}+\color{purple}{\sum_{j\neq m,n,p,q}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq j,m,n,p,q}^{1,k}\hat{F}_i:}\tag{6}\label{generalizedwick2}$$
and so on, for all possible contractions within that set of operators. If you sum all these results (notice the color code) from \eqref{generalizedwick0}, \eqref{generalizedwick1}, \eqref{generalizedwick2} and so on, you obtain on the LHS
$$\mathrm{LHS}=:\prod_{i=1}^k\hat{F}_i:\hat{F}_{k+1}+\underbrace{\Bigg(\color{navy}{\sum_{m,n}^{1,k}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq m,n}^{1,k}\hat{F}_i:+\sum_{m,n}^{1,k}\sum_{p,q\neq m,n}^{1,k}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq m,n,p,q}^{1,k}\hat{F}_i:}+\dots\Bigg)}_{\displaystyle\color{navy}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_k\}}}\hat{F}_{k+1}$$
whereas the RHS yields
$$\begin{align*}\mathrm{RHS}=&:\prod_{i=1}^{k+1}\hat{F}_i:+\underbrace{\Bigg(\color{green}{\sum_{m,n}^{1,k}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq m,n}^{1,k}\hat{F}_i\,\hat{F}_{k+1}:+\sum_{m,n}^{1,k}\sum_{p,q\neq m,n}^{1,k}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq m,n,p,q}^{1,k}\hat{F}_i\,\hat{F}_{k+1}:}+\dots\Bigg)}_{\displaystyle\color{green}{:\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k}\}\hat{F}_{k+1}:}}+\\
&+\underbrace{\color{purple}{\sum_{j}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}:\prod_{i\neq j}^{1,k}\hat{F}_i:+\sum_{m,n}^{1,k}\sum_{j\neq m,n}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}:\prod_{i\neq j,m,n}^{1,k}\hat{F}_i:+\sum_{m,n}^{1,k}\sum_{p,q\neq m,n}^{1,k}\sum_{j\neq m,n,p,q}^{1,k}\overset{\huge\frown}{\hat{F}_j\hat{F}_{k+1}}\overset{\huge\frown}{\hat{F}_m\hat{F}_{n}}\overset{\huge\frown}{\hat{F}_p\hat{F}_{q}}:\prod_{i\neq j,m,n,p,q}^{1,k}\hat{F}_i:}}_{\displaystyle\color{purple}{\overset{\hspace{1.8cm}\Huge\frown}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k}\}\hat{F}_{k+1}}}}
\end{align*}
$$
or equivalently
$$\mathrm{RHS}=:\prod_{i=1}^{k+1}\hat{F}_i:+\underbrace{\color{green}{:\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k}\}\hat{F}_{k+1}:}+\,\color{purple}{\overset{\hspace{1.8cm}\Huge\frown}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k}\}\hat{F}_{k+1}}}}_{\displaystyle\color{teal}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k+1}\}}}$$
since the normal-ordered sum of contractions of $k$ fermionic operators multiplied by the $(k+1)^\mathrm{th}$ operator plus the sum of contractions between this $(k+1)^\mathrm{th}$ operator and the normal-ordered sum of contractions of $k$ operators is precisely the normal-ordered sum of contractions between all $k+1$ operators.
Collecting all these results finally leads to
$$:\prod_{i=1}^k\hat{F}_i:\hat{F}_{k+1}+\displaystyle\color{navy}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_k\}}\hat{F}_{k+1}=:\prod_{i=1}^{k+1}\hat{F}_i:+\,\color{teal}{\mathcal{C}_N\{\hat{F}_1,\dots,\hat{F}_{k+1}\}}$$
and with this, Wick's theorem for $k+1$ is proven (these are the RHSs of \eqref{wickfork+1} and \eqref{wickforktimesk+1})! Notice that along this derivation, it was irrelevant if $\hat{F}$ was a creation $\hat{C}$ or annihilation $\hat{A}$ from the field operators $\hat{\phi}$ (this was nevertheless important in the derivation of Wick's lemma).
(Original post, contains the proof of Wick's lemma)
I would begin by trying to clarify some technical but important details about the field operators. You stated that $\hat{\phi}_k^-$ is the field operator associated to the negative energy and that it corresponds to the creation of an antiparticle, which is true. That index $k$, in the case of fermionic field operators, is just a notation for their momentum in Fock space $\vec{k}$ and spin $\sigma$, thus $k\equiv(\vec{k},\sigma)$. For simplicity, let the spin be forgotten. You then mention that you denote it as $\hat{\phi}_k^{-\dagger}$ but this is actually the field operator which annihilates an antiparticle. The operators $\hat{\phi}_k^-$ and $\hat{\phi}_k^{-\dagger}$ don't represent the same thing. The correct statement is that $\hat{\phi}_k^-$ and $\hat{\phi}_{-k}^{+}$ are equivalent. Put into words, this becomes: the creation of an antiparticle in a state $k$ is equivalent to the annihilation of a particle in a state $-k$. This is the particle hole picture translated to field operators.
Maybe this may be seen more clearly in the following manner: generically, the field operators are given by
$$\hat{\Phi}(\vec{r})=\sum_k u_k(\vec{r})\hat{a}_k,\quad \hat{\Phi}^\dagger(\vec{r})=\sum_k u_k^*(\vec{r})\hat{a}^\dagger_k$$
with the elementary operators $\hat{a}_k$ and $\hat{a}^\dagger_k$ satisfying specific anti-commutation relations for fermions. The elementary operators may be divided into particle or anti-particle operators, having positive or negative energy, or in momentum space positive and negative $|\vec{k}|$, or in the previously mentioned notation, simply opposite $k$. Let them be denoted as $\hat{a}_{k>0}\equiv\hat{\alpha}_k$ and $\hat{a}_{k<0}\equiv\hat{\beta}^\dagger_{-k}$, which lead to $\hat{a}^\dagger_{k>0}\equiv\hat{\alpha}^\dagger_k$ and $\hat{a}^\dagger_{k<0}\equiv\hat{\beta}_{-k}$. Thus, $\hat{\alpha}_k$ and $\hat{\alpha}^\dagger_k$ are elementary operators which create or annihilate particles with positive energies and $\hat{\beta}_{-k}$ and $\hat{\beta}^\dagger_{-k}$ operators which create or annihilate anti-particles having negative energies.
It is then possible to further express the field operators, after artificially introducing $\theta(k)+\theta(-k)=1$ and splitting the sum into two terms, as
$$\hat{\Phi}(\vec{r})=\underbrace{\sum\limits_{k<0}u_k(\vec{r})\hat{\beta}^\dagger_{-k}}_{\displaystyle \equiv\hat{\phi}_k^-(\vec{r})}+\underbrace{\sum\limits_{k>0}u_k(\vec{r})\hat{\alpha}_{k}}_{\displaystyle \equiv\hat{\phi}_k^+(\vec{r})}$$
Therefore, $\hat{\phi}_k^-$ creates an antiparticle in state $k$ and $\hat{\phi}_k^+$ annihilates a particle in state $k$, located at $\vec{r}$. Analogously
$$\hat{\Phi}^\dagger(\vec{r})=\underbrace{\sum\limits_{k<0}u_k^*(\vec{r})\hat{\beta}_{-k}}_{\displaystyle \equiv\hat{\phi}^{-\dagger}_k(\vec{r})}+\underbrace{\sum\limits_{k>0}u_k^*(\vec{r})\hat{\alpha}^\dagger_{k}}_{\displaystyle \equiv\hat{\phi}^{+\dagger}_k(\vec{r})}$$
where $\hat{\phi}_k^{-\dagger}$ annihilates an antiparticle in state $k$ and $\hat{\phi}_k^{+\dagger}$ creates a particle in state $k$, located at $\vec{r}$. This is why $\hat{\phi}^-_k$ and $\hat{\phi}^{-\dagger}_k$ represent different things and why $\hat{\phi}_k^-$ and $\hat{\phi}^+_{-k}$ are equivalent.
Notice that these are all expressed in the Schrodinger picture. Time dependence appears when one performs an unitary transformation to another picture, for example the interaction picture, such that
$$\hat{\Phi}_I(\vec{r},t)=\underbrace{\hat{\phi}^{-}_{kI}(\vec{r},t)}_{\displaystyle\mathrm{creation}}+\underbrace{\hat{\phi}^{+}_{kI}(\vec{r},t)}_{\displaystyle\mathrm{annihilation}},\quad\hat{\Phi}^\dagger_I(\vec{r},t)=\underbrace{\hat{\phi}^{-\dagger}_{kI}(\vec{r},t)}_{\displaystyle\mathrm{annihilation}}+\underbrace{\hat{\phi}^{+\dagger}_{kI}(\vec{r},t)}_{\displaystyle\mathrm{creation}}$$
Translated into your notations, dropping all the indices and dependence on position and time, you must have
$$\hat{\phi}_i=\hat{\phi}^+_i+\hat{\phi}^-_i,\quad\hat{\phi}^\dagger_i=\hat{\phi}^{+\dagger}_i+\hat{\phi}^{-\dagger}_i$$

Perhaps the general manner in which the Wick theorem is usually written, namely $\mathcal{T}\left\{\phi_1\cdot\dots\cdot\phi_n\right\}=\mathcal{N}\left\{\phi_1\cdot\dots\cdot\phi_n\right\}+\mathcal{C}_N\left\{\phi_1\cdot\dots\cdot\phi_n\right\}$ is a little confusing since it seems to contain only $\hat{\phi}_i$ field operators and no $\hat{\phi}^\dagger_i$. Here $\mathcal{T}$ denotes time-ordering, $\mathcal{N}$ normal-ordering and $\mathcal{C}_N$ the normal-ordered sum of all possible contractions.
To be more general, let us denote all types of fermionic field operators as $\left\{\hat{F}_i\right\}_{i=\overline{1,n}}$, where $\hat{F}_i$ can be either $\hat{\phi}_i^\pm$ or $\hat{\phi}^{\pm\dagger}_i$. Wick's theorem is more powerful and remains valid for all types of creation or annihilation parts from the fermionic field operators
$$\mathcal{T}\left\{F_1\cdot\dots\cdot F_n\right\}=\mathcal{N}\left\{F_1\cdot\dots\cdot F_n\right\}+\mathcal{C}_N\left\{F_1\cdot\dots\cdot F_n\right\}$$

Indeed, Wick's theorem is usually proven by induction. But before that, you need a way to express that "normal-ordered sum of all possible contractions" term. This is done by proving an auxiliary result, named Wick's lemma
$$\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}\hat{G}=\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\hat{G}\right\}+\sum_j\mathcal{C}\left\{\hat{F}_j,\hat{G}\right\}\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_{j-1}\hat{F}_{j+1}\cdot\dots\cdot\hat{F}_k\right\}$$
You have encountered this and got stuck at $\hat{F}_i\rightarrow\hat{\phi}_i^\pm$ and $\hat{G}\rightarrow\hat{\phi}^{-\dagger}_{k+1}$. As you can see, the results holds for any type of creation or annihilation fermionic field operators. There is an additional detail hidden here, which makes the computation slightly simpler: the time dependence of the operator $\hat{G}(t)$ is chosen such that $t<t_j\,\forall j=\overline{1,k}$ from $\hat{F}_j(t_j)$, hence time-ordering won't affect the involved products.
It is easier to first write the normal product as
$$\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}=(-1)^{\sigma_\pi}\underbrace{\hat{F}_{\pi_1}\cdot\dots\cdot\hat{F}_{\pi_l}}_{\displaystyle\mathrm{creation}}\underbrace{\hat{F}_{\pi_{l+1}}\cdot\dots\cdot\hat{F}_{\pi_k}}_{\displaystyle\mathrm{annihilation}}$$
where $\sigma_\pi$ is the parity of the permutation which rearranges the fermionic operators such that creation ones come before the annihilation ones. To simplify things even further, let us denote
$$\hat{C}_m\equiv\hat{F}_{\pi_m}\quad\mathrm{with}\,m=\overline{1,l},\quad\hat{A}_n\equiv\hat{F}_{\pi_n}\quad\mathrm{with}\,n=\overline{l+1,k}$$
Therefore, the normal product simply reads
$$\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}=(-1)^{\sigma_\pi}\hat{C}_1\cdot\dots\hat{C}_l\hat{A}_{l+1}\cdot\dots\cdot\hat{A}_k$$
There are only two cases, depending on $\hat{G}$.
If $\hat{G}=\hat{A}$ is an annihilation operator, it is immediately obvious that $\mathcal{N}\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\}\hat{A}=\mathcal{N}\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\hat{A}\}$. On the other hand, $\mathcal{C}\{\hat{F}_j,\hat{A}\}=\mathcal{T}\{\hat{F}_j,\hat{A}\}-\mathcal{N}\{\hat{F}_j,\hat{A}\}=\hat{F}_j\cdot\hat{A}-\hat{F}_j\cdot\hat{A}=0$, which assures Wick's lemma is satisfied in this case.
If $\hat{G}=\hat{C}$, one gets
$$\mathcal{N}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}\hat{C}=(-1)^{\sigma_\pi}\hat{C}_1\cdot\dots\hat{C}_l\hat{A}_{l+1}\cdot\dots\cdot\hat{A}_k\cdot\hat{C}$$
The idea is to simply make the last creation operator "jump" over its annihilating neighbours. Let us notice that in this case $\mathcal{C}\{\hat{A}_n,\hat{C}\}=\mathcal{T}\{\hat{A}_n,\hat{C}\}-\mathcal{N}\{\hat{A}_n,\hat{C}\}=\hat{A}_n\cdot\hat{C}+\hat{C}\cdot\hat{A}_n=0$. Therefore, each "jump" is done by replacing $\hat{A}_n\cdot\hat{C}=\mathcal{C}\{\hat{A}_n,\hat{C}\}-\hat{C}\cdot\hat{A}_n$. After all these replacements are performed and $\hat{C}$ reunites with his creation operator fellows, you obtain $\mathcal{N}\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\hat{C}\}$ and a sum of terms, each containing a contraction of the type $\mathcal{C}\{\hat{A}_j,\hat{C}\}$ multiplied by a normal product of the uncontracted operators $\mathcal{N}\{\hat{F}_1\cdot\dots\cdot\hat{F}_{j-1}\hat{F}_{j+1}\cdot\dots\cdot\hat{F}_k\}$. This is exactly what Wick's lemma states.
This result can be generalized in the following manner
$$\mathcal{N}_{mn}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}\hat{G}=\mathcal{N}_{mn}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\hat{G}\right\}+\sum_j\mathcal{C}\left\{\hat{F}_j,\hat{G}\right\}\mathcal{N}_{mn}\left\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\right\}$$
where $\mathcal{N}_{mn}\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\}$ is simply (an uninspired notation but it's quite difficult to write contractions like this) $\mathcal{N}\{\hat{F}_1\cdot\dots\cdot\hat{F}_k\}$ with the contraction $\mathcal{C}\{\hat{F}_m,\hat{F}_n\}$ inside and the rest of the operators left uncontracted. This can be generalized to as many contractions inside the normal product. If you continue this line of reasoning and write Wick's generalized lemma for more an more contractions, then you sum them all up, you obtain an expression for the sum of all possible contractions. This is exactly the term which appears in Wick's theorem!
The rest of the proof is just induction, you write Wick's theorem for $k$, aim to prove it for $k+1$ and use Wick's lemma repeatedly.

My personal opinion is that sometimes simplicity in physics computations is not a good thing. Dropping the time-dependence of time-ordered operators, trying to write the proof as condensed as possible, can actually lead to blockages. If you are interested, I have an extremely notation dense and rigorous proof of Wick's theorem. I tried to write a short version here, there are many more details that I completely skipped. I guess it turned out to be quite lengthy anyway...
