Jean Abou Samra (new account) on Nostr: nprofile1q…zdh59 The way I learnt it, you don't put any eta at all in the reduction ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyre3nlvve9v0ulm6elkwv5xpr6azl5f3n9u2c3fdjk4733lxa5ypgdzdh59 (nprofile…dh59) The way I learnt it, you don't put any eta at all in the reduction relation (or at most function eta). Decidability of type checking is proved by an algorithm that first reduces (so, with just beta and computation rules of eliminators), then compares the normal forms in a typed way.