If you are into constructive logic then this will only work for proving negative statements (where indeed the definition is the same as what a proof by contradi

If you are into constructive logic then this will only work for proving negative statements (where indeed the definition is the same as what a proof by contradiction would give you). For positive statements you won't get back a direct proof term of your initial statement, but rather a proof of a double negation of it.