fact: Definition itree_right t := match t with | itree_leaf n => arbitrary | itree_node t1 t2 => t2 end.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat