The Parigot encoding solves the Church encoding's problem of inefficient predecessor.\xa0 It can be typed using positive-recursive types, which preserve normalization of the type theory.