Here is a solution with truth values:
49 ALL(x):[Value(x) => [[x=t <=> x=f] => x=u]]
Rem DNeg, 48
------------------------------------ begin proof --------------------------------------
1 ALL(x):[Value(x) <=> x=f | x=t | x=u]
Axiom
2 ~f=t
Axiom
3 ~f=u
Axiom
4 ~t=u
Axiom
5 ~ALL(x):[Value(x) => [[x=t <=> x=f] => x=u]]
Premise
6 ~~EXIST(x):~[Value(x) => [[x=t <=> x=f] => x=u]]
Quant, 5
7 EXIST(x):~[Value(x) => [[x=t <=> x=f] => x=u]]
Rem DNeg, 6
8 ~[Value(w) => [[w=t <=> w=f] => w=u]]
E Spec, 7
9 ~~[Value(w) & ~[[w=t <=> w=f] => w=u]]
Imply-And, 8
10 Value(w) & ~[[w=t <=> w=f] => w=u]
Rem DNeg, 9
11 Value(w)
Split, 10
12 ~[[w=t <=> w=f] => w=u]
Split, 10
13 ~~[[w=t <=> w=f] & ~w=u]
Imply-And, 12
14 [w=t <=> w=f] & ~w=u
Rem DNeg, 13
15 w=t <=> w=f
Split, 14
16 ~w=u
Split, 14
17 [w=t => w=f] & [w=f => w=t]
Iff-And, 15
18 w=t => w=f
Split, 17
19 w=f => w=t
Split, 17
20 Value(w) <=> w=f | w=t | w=u
U Spec, 1
21 [Value(w) => w=f | w=t | w=u]
& [w=f | w=t | w=u => Value(w)]
Iff-And, 20
22 Value(w) => w=f | w=t | w=u
Split, 21
23 w=f | w=t | w=u => Value(w)
Split, 21
24 w=f | w=t | w=u
Detach, 22, 11
25 ~[w=f | w=t] => w=u
Imply-Or, 24
26 ~w=u => ~~[w=f | w=t]
Contra, 25
27 ~w=u => w=f | w=t
Rem DNeg, 26
28 w=f | w=t
Detach, 27, 16
29 ~w=f => w=t
Imply-Or, 28
30 ~w=f => ~w=t
Contra, 18
31 ~w=f
Premise
32 w=t
Detach, 29, 31
33 ~w=t
Detach, 30, 31
34 w=t & ~w=t
Join, 32, 33
35 ~~w=f
4 Conclusion, 31
36 w=f
Rem DNeg, 35
37 ~w=t => ~~w=f
Contra, 29
38 ~w=t => w=f
Rem DNeg, 37
39 ~w=t => ~w=f
Contra, 19
40 ~w=t
Premise
41 w=f
Detach, 38, 40
42 ~w=f
Detach, 39, 40
43 w=f & ~w=f
Join, 41, 42
44 ~~w=t
4 Conclusion, 40
45 w=t
Rem DNeg, 44
46 f=t
Substitute, 36, 45
47 f=t & ~f=t
Join, 46, 2
48 ~~ALL(x):[Value(x) => [[x=t <=> x=f] => x=u]]
4 Conclusion, 5
49 ALL(x):[Value(x) => [[x=t <=> x=f] => x=u]]
Rem DNeg, 48
------------------------------------ end proof --------------------------------------