Allow real includes inside ghost headers

[btj]

This allows ghost headers to use types declared by the real headers.

To maintain soundness, check at the point where the ghost header is included that the real headers included by the ghost header were already included earlier and therefore the real includes inside the ghost header are no-ops from the point of view of the global symbol table (assuming all headers have proper header guards).