proposition: Lemma filter_fix : forall s, infinitely_often P s -> filter s === Filter filter s.
proof: Proof. Proof using. applys~ (FixFunMod_mixed_partial (stream_family A) (measure (dist_to_next P)) (infinitely_often P) (@bisimilar A)). intros i s f1 f2 Ps H. simpls. destruct s. simpl. unfolds. destruct i. simple~. inverts Ps as Ps' Ev. case_if as C. simpl. constructor~. apply~ H. left*. inverts Ev as Ev. false. apply~ H. right. split~. forwards~: eventually_dist_cons Ev C. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat