Breaking subject reduction in Coq using positive coinductive types

bits.v

CoInductive bits : Set :=
| c0 : bits -> bits
| c1 : bits -> bits.

Lemma bits_eta : forall xs, match xs with
                     | c0 xs' => c0 xs'
                     | c1 xs' => c1 xs'
                     end = xs.
Proof.
  intro xs. destruct xs; reflexivity.
Defined.

CoFixpoint zeros : bits :=
  c0 zeros.

Compute (bits_eta zeros).

Check eq_refl
     : match zeros with
       | c0 xs' => c0 xs'
       | c1 xs' => c1 xs'
       end = zeros. (* fail *)

stream.v

CoInductive Stream : Set := go { hd : nat; tl : Stream }.

Lemma Stream_eta : forall xs : Stream, go (hd xs) (tl xs) = xs.
Proof.
  intro xs. destruct xs. reflexivity.
Defined.

CoFixpoint seq (n : nat) : Stream :=
  go n (seq (S n)).

Set Printing All.
Compute Stream_eta (seq 0).
(* = @eq_refl Stream (go (hd (seq O)) (tl (seq O)))
   : @eq Stream (go (hd (seq O)) (tl (seq O))) (seq O) *)
Definition Stream_eta_seq_0 : go (hd (seq 0)) (tl (seq 0)) = seq 0.
  try exact (@eq_refl Stream (go (hd (seq 0)) (tl (seq 0)))). (* fail *)
  exact (Stream_eta (seq 0)).
Defined.