b'
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.