Consider the following development:

```
Require Import Relation RelationClasses.

Set Implicit Arguments.

CoInductive stream (A : Type) : Type :=
| scons : A -> stream A -> stream A.

CoInductive stream_le (A : Type) {eqA R : relation A}
                      `{PO : PartialOrder A eqA R} :
                      stream A -> stream A -> Prop :=
| le_step : forall h1 h2 t1 t2, R h1 h2 ->
            (eqA h1 h2 -> stream_le t1 t2) ->
            stream_le (scons h1 t1) (scons h2 t2).

```

If I have a hypothesis `stream_le (scons h1 t1) (scons h2 t2)`, it would be reasonable for the `destruct` tactic to turn it into a pair of hypotheses `R h1 h2` and `eqA h1 h2 -> stream_le t1 t2`. But that's not what happens, because `destruct` loses information whenever doing anything non-trivial. Instead, new terms `h0`, `h3`, `t0`, `t3` are introduced into the context, with no recall that they are respectively equal to `h1`, `h2`, `t1`, `t2`.

I would like to know if there is a quick and easy way to do this kind of "smart `destruct`". Here is what i have right now:

```
Theorem stream_le_destruct : forall (A : Type) eqA R
  `{PO : PartialOrder A eqA R} (h1 h2 : A) (t1 t2 : stream A),
  stream_le (scons h1 t1) (scons h2 t2) ->
  R h1 h2 /\ (eqA h1 h2 -> stream_le t1 t2).
Proof.
  intros.
  destruct H eqn:Heq.
  remember (scons h1 t1) as s1 eqn:Heqs1;
  remember (scons h2 t2) as s2 eqn:Heqs2;
  destruct H;
  inversion Heqs1; subst; clear Heqs1;
  inversion Heqs2; subst; clear Heqs2.
  split; assumption.
Qed.

```