The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Suppose I have something like

  Lemma foo : equiv a'' (or a'' a')

Say I want to rewrite the first occurrence of a'' with (or a'' false).
When I do

  rewrite <- (or_id a'').

both occurrences of a'' are replaced (following Adam's suggestion I've
setup the setoid stuff for my boolean expressions). If I do

  pattern a'' at 1 ; rewrite <- (or_id a'')

it complains about the argument being in a covariant position.

  replace a'' at 1 with (or a'' false)

gives me a subgoal

  a'' = or a'' false

which is too strong (they are merely equivalent, not equal), and 
setoid_replace does not seem to have an 'at 1' option. 

Is there a way to apply the setoid rewriting to a particular occurrence
only?

Thanks,

Edsko