Question about the use of an inner forall

Hi, I am going to stop this discussion . What counts for me at this moment is that I know how it works. I thank everybody who replied to my email. As for the discussion about Curry Howard isomorphism and more about type theory, I shall gladly discuss these things further but than in private email. Hey, I hope really that I know how it works but this seems to be confirmed in these emails. I left Ocamel for Haskell for it's more functional approach. I think documentation about the features extending Haskell 98 is very needed for those who want only to program with the language Haskell. Thx for all replies Scott