Induction over a transitive relation in Coq
It is not clear to me how induction helps with the lemma you are trying to prove, so I'll take an alternative approach.

Firstly, I prove two helper lemmas that break apart and put back together ==&gt;  with --&gt; at the tail, rather than at the start. Based on these lemmas, I can manipulate the result using your definition of eval to get the desired result. My impression is that the core lemma relies too heavily on the somewhat odd definition of eval, which possibly allowed me to side-step any inductive argument you had in mind.

So, although the lemma you are interested in does not require induction over the transitive relation, the two helper lemmas do.

Note: proofs have not been optimised or beautified.

The first lemma inverts instances of t ==&gt; ti so that the single step reduction occurs at the end, rather than at the beginning. The proof relies on induction and was undemanding.

Lemma end_inversion :
  forall (t ti : State),
    t ==&gt; ti -&gt; 
    t = ti \/ 
      exists t', t ==&gt; t' /\ t' --&gt; ti.
Proof.
  intros.
  induction H.

  left; auto.

  destruct IHeval_trans; right.

  exists t.
  subst.
  split; [apply refl | auto].

  destruct H1 as [x [H1 H2]].
  exists x.
  split; auto.
  apply trans with (ti := ti); auto.
Qed.


The second lemma plugs a single step reduction onto the end of a transitive reduction to again get a transitive reduction. The proof is by straightforward induction. 

Lemma end_eval : 
  forall (t ti t' : State), 
    t ==&gt; t' -&gt; 
    t' --&gt; ti -&gt; 
    t ==&gt; ti.
Proof.
  intros.
  induction H.
  apply trans with (ti := ti); [auto | apply refl].
  apply trans with (ti := ti0); auto.
Qed.


And now your lemma. The proof relies on end_inversion to break up ==&gt;, does some manipulation of the result, and puts things back together using end_eval. No induction is required.

Lemma some_lemma :
  forall (a a' : Address) (m m' : Memory),
    (a, m) ==&gt; (a', m') -&gt;
    (a, m) ==&gt; (S a', m').
Proof.
  intros a a' m m' H.
  apply end_inversion in H.
  destruct H.
  inversion H; subst.
  apply end_eval with (t' := (a', m')).
    apply refl.
    apply eval_step; auto.
  destruct H as [x [H0 H1]].
  apply end_eval with (t := (a, m)) (t' := x); auto.
  inversion H1; subst.
  apply eval_step; auto.
Qed.