proposition: Lemma makeitree_fixpoint : forall m, itree_similar (makeitree m) (Makeitree makeitree m).
proof: Proof. Proof using. apply (FixFunMod_corec_total itree_family). reflexivity. apply itree_similar_eq. apply itree_family_COFE. introv H. unfold Makeitree. simpl. destruct x. auto. destruct i. auto. apply product_incr_similarity. apply H; simpl; auto with maths. apply H; simpl; auto with maths. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat