Logic: Proving ~(a ↔ b) and (a ↔ ~b) are equivalent in LPL's Fitch I am working on a proof where I was able to derive this general form: 

~(a ↔ b)

From this I would like to obtain:

a ↔ ~b

I have made sure that the two statements are equivalent by drawing out truth-tables. The problem is that I am not really sure how to go from the first statement to the second statement in Fitch. 
If it helps in answering the question, the specific proof I am working on is LPL's Exercise 8.50. It is the following: 
1.| Cube(b) ↔ (Cube(a) ↔ Cube(c))
2.| | Dodec(b)                            (assumption)
3.| | | Cube(a)↔Cube(c)                   (assumption)
4.| | | Cube(b)                           ↔Elim 1, 3
5.| | | ⊥                                 AnaCon 2, 4
6.| | ~(Cube(a)↔Cube(c))                  ~Intro 3-5
∴ Dodec(b) → (Cube(a) ↔ ¬Cube(c))

Lines 2-6 are my work. I know that this argument is valid because if b was anything besides a cube (a dodec or a tet), then if Cube(a), it would necessarily follow that ~Cube(c) and vice versa, because if Cube(a) implied Cube(c) or vice versa, it would necessitate that b would have to be a cube. 
 A: 0) $\lnot (a \leftrightarrow b)$ --- premise
1) $a$ --- assumed [a]
2) $b \to a$ --- from 1) by $\to$-intro
3) $b$ --- assumed [b]
4) $a \to b$ --- from 3) by $\to$-intro
5) $a \leftrightarrow b$ --- from 2) and 4)
6) $\bot$ --- from 0) and 5)
7) $\lnot b$ --- from 1) and 6) by $\lnot$-intro, discharging [b]

8) $a \to \lnot b$ --- from 1) and 7) by $\to$-intro, discharging [a].

9) $\lnot b$ --- assumed [c]
10) $b$ --- assumed [d]
11) $\bot$ --- from 9) and 10)
12) $a$ --- from 11)
13) $b \to a$ --- from 10) and 12) by $\to$-intro, discharging [d]
14) $\lnot a$ --- assumed [e]
15) $a$ --- assumed [f]
16) $\bot$ --- from 14) and 15)
17) $b$ --- from 16)
18) $a \to b$ --- from 15) and 17) by $\to$-intro, discharging [f]
19) $a \leftrightarrow b$ --- from 13) and 18)
20) $\bot$ --- from 0) and 19)
21) $a$ --- from 14) and 20) by Double Negation, discharging [e]

22) $\lnot b \to a$ --- from 9) and 21) by $\to$-intro, discharging [c]

23) $a \leftrightarrow \lnot b$ --- from 8) and 22).


A: One direction of the equivalence is relatively easy to show: $A ↔ ¬B ∴ ¬(A ↔ B)$. The basic plan is to negate the goal, derive a contradiction which will then allow one to derive the goal.
Here is a proof using a Fitch-style natural deduction proof checker:

To show the other direction is more involved. Again, one can negate the goal, $A ↔ ¬B$, but one should rewrite the goal as a conjunction of disjunctions, $(¬A ∨ ¬B) ∧ (A ∨ B)$, so one can use other inference rules. Once one reaches a contradiction this will give one the rewritten goal from which one can derive the desired biconditional.  
Here is a proof of the other direction, $¬(A ↔ B) ∴ A ↔ ¬B$:

For the proof checker and the associated textbook see the links below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
