Jean Abou Samra (new account) on Nostr: nprofile1q…zdh59 What do you mean? I'm talking about strong normalization, i.e., ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyre3nlvve9v0ulm6elkwv5xpr6azl5f3n9u2c3fdjk4733lxa5ypgdzdh59 (nprofile…dh59) What do you mean? I'm talking about strong normalization, i.e., termination of reduction, not canonicity. This is what you need for decidability of type checking. And axioms are not a problem there.