proposition: Lemma const1_fix : const1 === Const1 const1.
proof: Proof. Proof using. applys~ (FixValMod_fix (stream_family nat)). typeclass. intros i 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