proposition: Lemma stream_mod_similarity : forall A (E:binary A), bisimilar_mod E = similar (stream_mod_family E).
proof: Proof. Proof using. extens. intros s1 s2. unfold similar. simpl. split. intros. apply~ bisimilar_mod_to_upto. intros. apply~ bisimilar_mod_take. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat