[TYPES] Encoding of negation

[Philip Wadler]

Here is your argument again.

1.  all Z. (A+ -> Z) -> Z) |- all Z. A+
2.  (A+ -> B) -> B |- A+               (eliminate "all")

I repeat, that even if A+ does not contain Z, it is not permissible to 
conclude 2 from 1.  If you want to conclude 2 from 1, you need to tell 
me how you derive it.  The statement 'eliminate all' is not a correct 
justification!  Yours (frustrated),  -- P

-- 
  \ Philip Wadler, Professor of Theoretical Computer Science
  /\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/