Using Fitch to proof ∀x Indiff(x,x). Help I am having a hard time solving this Fitch Proof.
Goal: ∀x Indiff(x,x)
I have to proof this goal using the following four premises: (might not need all of them)
P1: ∀x∀y(WeakPref(x,y)∨WeakPref(y,x))
P2: ∀x∀y∀z((WeakPref(x,y)∧WeakPref(y,z))→WeakPref(x,z))
P3: ∀x∀y(StrongPref(x,y)↔ ¬WeakPref(y,x))
P4: ∀x∀y(Indiff(x,y)↔(WeakPref(y,x)∧WeakPref(x,y)))
Here is how far I've gotten right now

I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form, but if I delete the premise in the subproof, I have no idea how to bring out ∀x Indiff(x,x).
Any suggestion is appreciated.
Thank you!
 A: If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$\begin{array}{|l}\forall x~\forall y ~Q(x,y)\\\forall x~\forall y ~R(x,y)\\\hline \begin{array}{|l}\boxed c\\\hline \forall y~Q(c,y)\\Q(c,c)\\ \forall y~ R(c,y)\\ R(c,c)\\~~\vdots\\ P(c,c)\end{array}\\\forall x~P(x,x)\end{array}$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.

@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).

The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it.   You then use universal elimination, and so derive $\text{WeakPref}(c,c)\land\text{WeakPref}(c,c)$ from $\text{WeakPref}(c,c)\lor\text{WeakPref}(c,c)$ to prepare for the biconditional elimination. 
$\def\oto{\leftrightarrow}\begin{array}{|l}\forall x~\forall y ~(\text{WeakPref}(x,y)\lor\text{WeakPref}(y,x))\\\forall x~\forall y~(\text{StrongPref}(x,y)\to \lnot\text{WeakPref}(y,x))\\\forall x~\forall y ~(\text{Indiff}(x,y)\oto(\text{WeakPref}(x,y)\land\text{WeakPref}(y,x)))\\\hline \begin{array}{|l}\boxed c\\\hline \forall y~(\text{WeakPref}(c,y)\lor\text{WeakPref}(y,c))\\\text{WeakPref}(c,c)\lor\text{WeakPref}(c,c)\\\forall y~(\text{StrongPref}(c,y)\oto \lnot\text{WeakPref}(y,c))\\\text{StrongPref}(c,c)\oto\lnot\text{WeakPref}(c,c)\\ \forall y~ (\text{Indiff}(c,y)\oto(\text{WeakPref}(c,y)\land \text{WeakPref}(y,c)))\\ \text{Indiff}(c,c)\oto(\text{WeakPref}(c,c)\land\text{WeakPref}(c,c))\\~~\vdots\\ \text{WeakPref}(c,c)\land\text{WeakPref}(c,c)\\\text{Indiff}(c,c)\end{array}\\\forall x~\text{Indiff}(x,x)\end{array}$
