Alt.v

Axiom A :Set.
CoInductive Stream := Cons : A -> Stream -> Stream.

Definition head (s:Stream) : A :=
   match s with
    Cons x _ => x
  end.

Definition tail (s:Stream) : Stream :=
  match s with
    Cons _ xs => xs
  end.

Inductive eq {A:Type} (x:A) : A ->Prop := eq_refl : eq x x.

CoInductive Bisim : Stream -> Stream -> Prop := 
  B : forall (s t : Stream), eq (head s) (head t) -> Bisim(tail s) (tail t) -> Bisim s t.

CoFixpoint replicate (x:A) := Cons x (replicate x).

CoFixpoint alt (s t :  Stream) :=
  match s, t with
    Cons x xs, Cons _ ys => Cons x (alt ys xs)
  end.

Theorem eq_alt : forall (x:Stream), Bisim x (alt x x).
cofix. 
intros.
destruct x.
constructor.
simpl.
constructor.
simpl.
apply eq_alt.
Qed.