proposition: Lemma pconst_spec : forall A {IA:Inhab A} (x:A), LibStream.const x === pconst x.
proof: Proof. Proof using. intros. apply bisimilar_mod_take. induction i. simple~. apply* sym_inv. apply* trans_sym_lr. apply bisimilar_mod_to_upto. apply pconst_fix. simpl. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat