FYI, the logic program I use cannot do contradiction introductions. This point is most likely irrelevant, for I highly doubt I would need to use any form of contradiction for this proof.
In my attempt to solve this, I started off with assuming (p ⇒ q) ⇒ p)
Is this correct?
If so, what next? Forgive me if the solution seems so obvious.