If congruence is true for all substitutions then to prove it isn't true I only need to find a single example where it cannot be proven from what I have, which is only "steps to the same thing" and eta

It's the substitution of the first convertibility into the application (h y) where y has the function type, so it should hold by congruence, but it doesn't, because it's not the steps-to-same-thing rule (it doesn't step) and it's not eta (doesn't step to a syntactic function)

jonoodle@ionchy@types.plIt's the substitution of the first convertibility into the application (h y) where y has the function type, so it should hold by congruence, but it doesn't, because it's not the steps-to-same-thing rule (it doesn't step) and it's not eta (doesn't step to a syntactic function)