Derivation using Fitch

I'm working on some problems on natural deduction, sadly I'm stuck with this one.
In our system we're allowed to rewrite P v Q to ~P => Q, '~' represents the 'not' connective:

Code:

---

Show that: (P <=> Q) => ((P ^ Q) v (~P ^ ~Q))

(P => Q) ^ (Q => P)                            [ 1: H]
    ~(P ^ Q)                                    [ 2: H]

        ~P                                      [ C - 4: ?
        ~Q                                      [ C - 3: ?

    ~P ^ ~Q
    ~(P ^ Q) => (~P ^ ~Q)                      [ C - 2: =>I  2, C - 3]
    (P ^ Q) v (~P ^ ~Q)                        [ C - 1: v, C - 2]
(P <=> Q) => ((P ^ Q) v (~P ^ ~Q))              [ C: => 1, C-1]

---

I keep getting stuck between 2 and C - 2, and basically I'm not sure if I should eliminate the ^ in the first hypotheses. My intuition tells me I've to work something in with RAA, but I can't seem to figure out what and how. Any help would be, again, greatly appreciated!

The first thing that comes to mind is to convert P => Q into ~P \/ Q and Q => P into ~Q \/ P and then use disjunction elimination rule to consider all four combinations: ~P and ~Q, ~P and P, Q and ~Q, Q and P. The second and third combinations imply contradiction, from which you can derive anything, including P /\ Q \/ ~P /\ ~Q.

Hmm, ex falso isn't part of this method, we're supposed to solve disjunction by rewriting it to an implication.
Which brings me to my next question:

Code:

---

Derive: ((P => Q) => ~P) => (P => ~Q)
(P => Q) => ~P                                      [ 1, H]
    P                                                [ 2, H]
        Q                                            [ 3, H]
{Now, I've to conclude false from Q. I have  both a P and a ~P in my premiss,
from which I can derive a contradiction.
But, how am I allowed to eliminate the ~P from 1?
Since I have both P and Q assumed I would say I actually have  P => Q,
on the other hand, introducing the => means I;ve to end the assumption 'Q'.
^-Intro isn't useful either? Or is it possible to eliminate
the P=>Q on the basis that P ^ Q is a stronger proposition than P=>Q?
I know I've to 'get' the ~P, but I'm not sure by which rule I'm allowed to do this.}

{ One possibility I've explored is this: }
            P => Q      [H]
                ~P        [ =>E 1]
                False      [Contradiction P, ~P]
          ~(P => Q)  [False Intro on P => Q and False]
            False        [Contradiction P=>Q, ~(P =>Q), but is this allowed???]
        ~Q
    P => ~Q
((P => Q) => ~P) => (P => ~Q)

---