Set Asymmetric Patterns.

Section Specified_Streams.
CoInductive SStream (A : Set) : (nat → A → Prop) → Set :=
    scons :
      ∀ (P : nat → A → Prop) (a : A),
      P 0 a → SStream A (fun n : nat ⇒ P (S n)) → SStream A P.

Variable A : Set.

Definition shd (P : nat → A → Prop) (x : SStream A P) :=
  match x with
  | scons _ a _ _ ⇒ a
  end.

Definition stl (P : nat → A → Prop) (x : SStream A P) :=
  match x in (SStream _ P) return (SStream A (fun n : nat ⇒ P (S n))) with
  | scons _ _ _ s ⇒ s
  end.

Fixpoint snth (n : nat) : ∀ P : nat → A → Prop, SStream A P → A :=
  fun (P : nat → A → Prop) (s : SStream A P) ⇒
  match n with
  | O ⇒ shd P s
  | S m ⇒ snth m (fun n : nat ⇒ P (S n)) (stl P s)
  end.

End Specified_Streams.