On Tue, 2013-02-26 at 16:37 +0000, Lawrence Paulson wrote: > I guess you are saying that this dangling type dependence introduces a > function type in the first line. It does; you can write term "..." after the first proof step to see this more explicitly. Tjark