proposition: Lemma nats_fix : forall (n:nat), nats n === Nats nats n.
proof: Proof. Proof using. intros. applys (FixFunMod_corec (stream_family nat) (@pred_true nat)); autos*. apply stream_cofe. clears n. intros i n s1 s2 _ H. simpls. destruct~ i. unfolds. simpl. constructor~. apply* H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat