Levy Labels and Recursive Types

摘要

In this note we introduce a generalization of the Levy label technique which applies easily to lambda calculus with beta-eta conversion and lambda calculus with surjective pairing a' la PSP.