proposition: Lemma stream_mod_cofe : forall A {IA:Inhab A} (E:binary A), equiv E -> COFE (stream_mod_family E).
proof: Proof. Proof using. introv IA Equiv. apply nat_cofe. typeclass. intros. apply~ equiv_bisimilar_mod_upto. introv H. exists (diagonal (fun i => u (S i)) 0). induction i; unfolds. simple~. apply~ bisimilar_mod_upto_succ. apply~ (trans_sym_rl (u i)). rewrite stream_diagonal_nth. math_rewrite~ (i + 0 = i). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat