Simply typed λ calculus with surjective pairing StatmanRichard 1992 Mathematics Technical Report