Andrej Bauer is a red flag (Was: How to prove this theorem with intuitionistic natural deduction?)

Hi,
 > Meanwhile, you might have seen it, I have also asked on SE:
 > <https://proofassistants.stackexchange.com/questions/4455/negative-translation-for-linear-propositional-logic>
Sorry, but I must quite. Anything where Andrej Bauer is
a red flag. I remember he was censoring some post of mine,
don't remember exactly where it was.
You can try searching here:
https://groups.google.com/g/sci.logic/search?q=Andrej%20Bauer%20
Julio Di Egidio schrieb:

Dear logicians,
 How to prove the following theorem with natural deduction in intuitionistic propositional logic (namely, no classical inference rules)?
    `(P -> Q -> R) |- (P /\ Q -> R)`
 Thanks for any help.
 -Julio