[TYPES] Encoding of negation

[Peter Selinger]

Vladimir Komendantsky wrote:
> 
> You couldn't have ever expected Gamma |- B classically iff Gamma* |- B*
> intuitionistically because this is false for your definition of *.

It certainly holds for the Hofmann-Streicher-Reus translation, and
also for Goedel's translation. The right-to-left implication is
trivial in those cases because in each case, A = A** holds
classically.

-- Peter