Par is now defined as an expression of type [∀ X, expr X] (instead of a
value) and we prove that it is stable under weakening and substitution.