Coq: destruct (co)inductive hypothesis without losing information

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.