[Agda] Re: Associativity for free!

[Andrea Vezzosi]

On Sat, Nov 5, 2011 at 8:14 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> Fair enough, if you phrase the Kripke structure in terms of subcontext
> inclusion rather than context extension, then I can see how it goes through
> without worrying about associativity.

Exactly, and arbitrary renamings seem to do the work here (scroll to
the bottom):
 http://code.haskell.org/~Saizan/WellTypedTerms.agda