The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Actually, here's an even simpler solution, based on the structure of 
your theorem.

Hint Constructors eval_trans.
Hint Extern 1 (_ --> _) => apply eval_step.

Lemma gt_S : forall n, S n > n.
  auto.
Qed.

Hint Resolve gt_S.

Lemma some_theorem' :
  forall S1 S2, S1 ==> S2
    -> S1 ==> (S (fst S2), snd S2).
  induction 1; intuition subst;
    eauto; match goal with
             | [ t : State |- _ ] => destruct t; eauto
           end.
Qed.

Theorem some_theorem :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==> (a', m') ->
    (a, m) ==> (S a', m').
  intros ? ? ? ? H; apply some_theorem' in H; auto.
Qed.