diff --git a/theories/streams.v b/theories/streams.v
index 4b4622a7312481671b8c943d12d5c5d66bd256cc..d07e76b60f5772805d14febca2242b63ada7c085 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -23,6 +23,12 @@ Fixpoint slookup {A} (i : nat) (s : stream A) : A :=
   match i with O => shead s | S i => stail s !.! i end
 where "s !.! i" := (slookup i s).
 
+Global Instance stream_fmap : FMap stream := λ A B f,
+  cofix go s := f (shead s) :.: go (stail s).
+
+Fixpoint stake {A} (n : nat) (s : stream A) :=
+  match n with 0 => [] | S n => shead s :: stake n (stail s) end.
+
 Section stream_properties.
 Context {A : Type}.
 Implicit Types x y : A.