Short answer: Yes—adding “bisimilarity implies Leibniz equality” for (non-indexed, strictly positive) coinductive datatypes such as streams is consistent with Coq’s logic. It is not provable in intensional Coq in general, but it holds in standard set-theoretic models and therefore is consistent relative to Coq.

Why it is reasonable

• For a coinductive datatype given as the greatest fixed point νF of a functor F (e.g., streams for F(X) = A × X), the canonical notion of bisimulation is the largest relation preserved by the destructors. In category-theoretic terms, on a final F-coalgebra, bisimilarity coincides with equality: any bisimulation R on νF factors through the unique coalgebra maps into νF, and by finality the two projections from R into νF must be equal, hence related elements are equal. So “bisimilarity ⇒ equality” is exactly the statement that your coinductive type behaves as a final coalgebra.
• In set-theoretic semantics (Set), coinductive types for polynomial functors are interpreted as final coalgebras (streams are A^ω, coinductive trees are sets of possibly infinite trees, etc.). Equality there is ordinary set-theoretic equality, and bisimilarity indeed equals equality. Thus your axiom is valid in that model.

Consequences and caveats

• In Coq you can always prove the easy direction equality ⇒ bisimilarity (by substituting and using a coinductive reflexivity proof). The converse (your axiom) is not derivable in general, which is why libraries usually treat bisimilarity as a setoid equality and avoid turning it into Leibniz equality.
• Adding the axiom lets you rewrite with = instead of maintaining a separate setoid relation. For streams, you can derive “eta” for free: s = Cons (hd s) (tl s), since those are bisimilar. This is not contradictory for coinductive types.
• The axiom does not conflict with UIP or with functional extensionality; it’s compatible with the usual intensional equality of Coq. It also does not force definitional (convertibility) equality—only propositional equality.
• For indexed coinductive families, you would want the appropriate dependent version (e.g., equality in the appropriate slice), but the same idea remains consistent in standard models.
• Your opening sentence should say “largest bisimulation,” not “largest equivalence relation.”

References (for the coalgebraic fact)

• J.J.M.M. Rutten, Universal Coalgebra: A Theory of Systems (Theorem/Prop.: bisimilarity equals equality on final coalgebras).
• P. Aczel and N.P. Mendler, A final coalgebra theorem (and subsequent literature on polynomial functors and their final coalgebras).

Bottom line For coinductive datatypes like streams, the axiom Stream_bisim xs ys -> xs = ys is consistent with Coq’s logic (and true in standard models). It’s a useful extensionality principle if you are comfortable working modulo this additional axiom.