Post #1942217

@MartinEscardo That's just what I (jokingly) meant in the next sentence ;) So yes to some extent it is, since this is very much me trying to make sense of proof theory I am re-casting it with my own words. But somehow what I wanted to put forward is that it brought a new (to me) light on something (bidirectional typing) I already understood, by looking at it in a different context. It's probably a bit pretentious a claim at this stage, but I feel this is a tentative new entry in the Curry-Howard correspondence, which, as we know, is a nice way to understand things we think we know.