Require Stlc.
Import Stlc.
Import Stlc.STLC.

Inductive count_step:  nat*tm -> nat*tm -> Prop :=
 cs1: forall n t t', step t t' -> count_step (n,t) (S n, t').

Notation count_steps := (refl_step_closure count_step).

Theorem erase_count:
  forall n t n' t', count_steps (n,t) (n',t') -> stepmany t t'.
Proof.
(* FAILED PROOF ATTEMPT #1: 
 induction 1.
  Fails because the arguments of count_steps are not simple variables.
  END FAILED PROOF ATTEMPT #1*)

(* FAILED PROOF ATTEMPT #2: 
  intros.
  induction H.
  Fails because the arguments of count_steps are not simple variables.
  END FAILED PROOF ATTEMPT #2*)

(* FAILED PROOF ATTEMPT #3:  
  intros.
  remember (n,t) as nt.
  remember (n',t') as nt'.
 (* Although nt and nt' are variables, this will fail because there are other
  mentions of nt and nt'   "above the line." *)
  induction H.
  subst. inversion Heqnt'. subst. apply rsc_refl.
  subst.
  (* We can't prove that  y=(n,t), so we won't be able to use the induction hyp. *) 
 END FAILED PROOF ATTEMPT #3*)

intros.
remember (n,t) as nt.
remember (n',t') as nt'.
revert n t Heqnt n' t' Heqnt'.
(* NOW: the inductive predicate count_steps is applied just to _variables_
   nt and nt'.   There are no other mentions of nt and nt' above the line.
   There are some mentions of nt and nt' below the line. *)
induction H; intros.
subst. inversion Heqnt'; auto.
subst.
destruct y as [n1 t1].
specialize (IHrefl_step_closure n1 t1 (refl_equal _) n' t' (refl_equal _)).
apply rsc_step with t1; auto.
inversion H; auto.
Qed.