proposition: Lemma pconst_fix : forall A {IA:Inhab A} (n:A), pconst n === PConst pconst n.
proof: Proof. Proof using. intros. applys* (FixFunMod_corec (stream_family A) (@pred_true A)). 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