proposition: Lemma uv_fix : mu === MU mu mv /\ mv === MV mu mv.
proof: Proof. Proof using. applys (FixValModMut2_fix (prod_family (stream_family nat) (stream_family nat))). rewrite~ prod2_eq_tuple_proj. unfold bisimilar. rewrite stream_mod_similarity. apply prod_similar. apply prod_cofe; typeclass. intros i u1 v1 u2 v2 H. simpls. destruct~ i. split. unfolds. simpl. constructor~. apply* H. unfolds. simpl. constructor~. destruct i. simple~. simpl. constructor~. apply* H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat