The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

In the standard library (theories/Init/Logic.v), there is this:

  Theorem and_cancel_l : forall A B C : Prop,
    (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
  Proof.
    intros; tauto.
  Qed.

As part of the exercise, I have tried to create a corresponding proof-script 
without automation.

At one point, I was in this state:

  1 subgoal
  A : Prop
  B : Prop
  C : Prop
  H1 : B <-> C
  ______________________________________(1/1)
  C /\ A -> B /\ A

and yearned to make the following step:

        replace all occurrences of "B" with "C" (this step is justified by 
"H1 : B <-> C"

and find myself here:

  1 subgoal
  A : Prop
  B : Prop
  C : Prop
  H1 : B <-> C
  ______________________________________(1/1)
  C /\ A -> C /\ A

Is there a tactic that would allow me/us to do this kind of step?
(just like as we can take advantage of equalities by "rewrite" tactics.)