fact: CoInductive itree : Type := | itree_leaf : nat -> itree | itree_node : itree -> itree -> itree.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat