Elim on a variable already in the context?

[favonia]

trafficstars

@jonsterling

[jonsterling]

My first thought is to not support this directly until we have some sick tactics that can generalize the goal properly --- it is not enough to generalize the goal using generalize, since we need to reformulate the generalized goal into a Kan type code. All this is possible, but it's currently a little tricky.