proposition: Lemma stream_cofe : forall A {IA:Inhab A}, COFE (stream_family A).
proof: Proof. Proof using. intros. apply~ stream_mod_cofe. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat