Yeah, I suppose I was playing fast and loose with the terminology to make it more approachable. iirc, the definition of proof by contradiction is you assume the negation, show that the negation has something that is both true and not true, and hence the negation is logically unsound. Since you can technically derive anything from an unsound system, you derive that the negation is false, and then by the laws of excluded middle and non-contradiction, you know that p must be true.

But now I see from what you mentioned that this means that if you don't do the negation elimination, then you can still show `¬¬p` in an intuitionistic logic system.

Is proof by contradiction of a false statement just a counterexample? Because a counterexample shows that the statement is incoherent, so the negation must be true. And you have to construct a counterexample.

A counterexample as generally understood would be a constructive refutation. Proof by contradiction is much more general than that. Of course the problem of extracting the residual constructive content from a proof by contradiction (explaining how it is in some sense constructing some vastly generalized counterexample) is non-trivial.