[ceh123]

Okay yup, turns out this is correct and it's slightly upsetting to me honestly haha. Just for someone else if they're interested where contrapositive and contradiction both use law of excluded middle (the ==* step requires it):

Contrapositive:

A-> B == A or ~B == ~B or A ==* ~B or ~(~A) == ~B -> ~A

Contradiction:

~(~A and B) == ~~A or ~B ==* A or ~B == A -> B

[housecarpenter]

You might be interested to know that in intuitionistic logic, you still have a one-sided contrapositive law, i.e. (A > B) > (~B > ~A):

  [1] A > B(assumption)
  [2] ~B (assumption)
  [3] A (assumption)
  [4] B (modus ponens on 1 and 3)
  [5] ~A (proof of negation on 3, 4 and 2)

It's only the converse that no longer holds. In general familiar equivalences from classical logic are still valid in intuitionistic logic but only in one direction.