proposition: Lemma const_fix : forall n, const n === Const const n.
proof: Proof. Proof using. intros. applys (FixFunMod_corec (stream_family nat) (@pred_true nat)); autos*. apply stream_cofe. clear 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