Yes – adding an axiom that identifies two coinductive values that are bisimilar with Leibniz equality does not lead to inconsistency. Just as with the more familiar “functional extensionality” axiom, the principle is independent of Coq’s core logic (it cannot be proved inside Coq), but it is consistent with it: there is a standard model of the Calculus of Inductive Constructions in which the axiom is true.

Why the axiom is not provable
————————————————— With an intensional equality, two closed terms are equal only when they reduce to convertible normal forms. Two differently-defined streams that unfold to the same sequence (for instance

CoFixpoint s₁ := Cons 0 s₁.
Definition  s₂ := Cons 0 s₂.

) are not convertible, hence Coq cannot prove s₁ = s₂, although they are evidently bisimilar. A proof of your axiom would enlarge the conversion relation, which is why it is not derivable in the current type theory. Nothing, however, forbids us to add the propositional equality as an extra postulate.

A model that validates the axiom
——————————————— Take the usual set-theoretic semantics that is used to establish Coq’s own consistency (types ↦ sets, terms ↦ elements, = ↦ set-theoretic equality).

Streams.
Interpret

Stream A    :=  ℕ → ⟦A⟧

(that is, infinite sequences, or functions from the natural numbers to the set ⟦A⟧ interpreting A). The constructor is

Cons a σ  ↦  λ n. if n = 0 then a else σ (n-1).

In this model two sequences are set-theoretically equal iff they return the same element of ⟦A⟧ at every position, i.e. iff they are bisimilar. Consequently

⟦Stream_bisim A xs ys⟧  ⇒  xs = ys

holds, so your axiom Stream_bisim_eq is satisfied.

General coinductive data.
For a coinductive type that is the final coalgebra of a strictly positive functor F (all the coinductive types you can declare in Coq), interpret it as the usual final coalgebra in Set. In that semantics the largest bisimulation equals ordinary equality, hence the corresponding extensionality axiom is also true. Therefore the whole family of axioms

∀ x y : νF,  bisim_F x y → x = y

is sound in the model.

Because the model is exactly the one Coq’s meta-theory relies on for its own consistency, adding an axiom that is satisfied in that model cannot introduce a contradiction. Formally:

1. If Coq + ZFC is consistent,
2. and axiom P is true in the standard model of Coq built in ZFC,
3. then Coq + P is consistent as well.

(Bisim-extensionality meets condition 2.)

Relationship with other extensionality principles
——————————————————————————— • It is analogous to functional extensionality: neither follows from pure CIC, both are validated by the same set-theoretic model, and each can safely be assumed as an additional axiom.

• It is weaker than univalence and does not require any large-cardinal assumptions.

What you gain / what you do not break
——————————————————————— • You can reason equationally about streams (or other coinductive objects) using the usual rewriting facilities once you have proved bisimilarity.

• You do not turn propositional equality into definitional equality, so computation, extraction, and termination properties of Coq are unaffected.

• You do not obtain any ability to prove False; all classical meta-results for Coq remain valid.

Conclusion
─────────── The axiom

Stream_bisim A xs ys → xs = ys

and, more generally, “bisimilar coinductive values are equal”, is consistent with Coq’s logic; feel free to add it if it makes reasoning about your coinductive objects more convenient.