Short answer
Yes, nothing contradictory is known to follow from the axiom

Stream_bisim A xs ys  ->  xs = ys

(or the analogous axiom for any other guarded co-inductive type).
In the usual set–theoretic model of Coq the axiom is actually true, so adding it to Coq can only be inconsistent if Coq itself already is.

Why the axiom is true in a classical model

1. How streams are interpreted.
   In the standard model (ZFC, sets in Set and propositions in Prop) the polymorphic stream type

   CoInductive Stream A := Cons : A -> Stream A -> Stream A

is interpreted as the set of infinite sequences
Stream A ≅ ℕ → A.

The destructor

   head : Stream A -> A
   tail : Stream A -> Stream A

is interpreted as the obvious projection on sequences, and the pair
σ ↦ (head σ , tail σ) makes (Stream A, Cons) the final F-coalgebra for the functor F X = A × X.

2. What a bisimulation is.
   A relation R ⊆ S × S is a bisimulation if there is a function

   r : R -> A × R

whose first (resp. second) projection is head (resp. tail) composed with the first (resp. second) projection R → S. Concretely, (σ,τ) ∈ R implies head σ = head τ and (tail σ , tail τ) ∈ R.

3. In any category, if (S,s) is a final F-coalgebra and R ⊆ S × S is a bisimulation, both projections

   π₁ , π₂ : R -> S

are coalgebra morphisms. Finality of (S,s) therefore forces

   π₁ = π₂.

But π₁(x,y)=x and π₂(x,y)=y, so x = y for every (x,y)∈R. Hence every bisimulation is contained in equality; the largest bisimulation is equality itself.

Therefore the statement

   (σ,τ) bisimilar  ⇒  σ = τ

is valid in the set-theoretic model.

Consequences for consistency

Because the axiom is satisfied in a model in which Coq’s rules are interpreted, it cannot introduce a contradiction unless those rules are already contradictory. In other words

Coq consistent ⇒ Coq + Stream_bisim_eq consistent.

Relation with other extensionality principles

• For functions, “pointwise equal ⇒ equal” is functional extensionality. It is also true in the set model and is widely assumed to be consistent with Coq.
• For coinductive data, “bisimilar ⇒ equal” is an analogous extensionality principle.

Just as functional extensionality cannot be proved inside intensional type theory, bisimulation extensionality is not provable in vanilla Coq, but adding it as an axiom is perfectly safe from the point of view of consistency.

Generalisation

The argument does not rely on any property specific to streams.
For every coinductive type defined in Coq by

CoInductive νF := constructor …

where F is a strictly positive functor, the same reasoning shows that in the set model the largest bisimulation on νF is equality. Hence the schema

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

can be added without threatening consistency.

So, your intuition was right: two bisimilar streams cannot be distinguished by any observation, and postulating their equality is consistent with Coq’s logic.