Properly compute the projection (face) of lambda.

Makes the impredicative natural example pass.

This is experimental; should be reviewed carefully
don't take the face twice.
simplify
Merge branch 'param2experiment' into parametricity2