fact: Definition Product product m1 m2 := match m1,m2 with | itree_node t11 t12, itree_node t21 t22 => itree_node (product t11 t22) (product t12 t21) | _, _ => itree_node m1 m2 end.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat