The tactic of generalizing \neg A to A\to C does not work to prove all classically valid statements involving double negations. Note that any schema of the syntactic shape (A\to C)\to B is too strong to be provable: If it were provable, then any true proposition C would prove any other proposition B. Now a variant of interest here is where A be replaced by (B\to C). It shows, possibly unsurprisingly, that the naive generalization of the double negation elimination \neg \neg B\to B cannot be provable in this way.
