The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Suppose one has a goal of the form:

  <some expression with free X> = ?42 X

where ?42 is an evar with the proper function type.  Is there a way to 
abstract out X from just the lhs of the equality (via beta expansion)?  
Like a variant of pattern that could be focused on just the lhs of the 
equality, allowing ?42 X to unify easily with the resulting beta-expansion?

-- Jonathan