proposition: Lemma stream_similarity : forall A, @bisimilar A = similar (stream_family A).
proof: Proof. Proof using. intros. apply stream_mod_similarity. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat