From Tealeaves Require Export
  Classes.Kleisli.ContainerMonad
  Classes.Kleisli.TraversableMonad
  Classes.Kleisli.Theory.TraversableFunctor
  Classes.Kleisli.Theory.ContainerMonad.

Import Monoid.Notations.
Import Applicative.Notations.
Import TraversableFunctor.Notations.
Import TraversableMonad.Notations.
Import ContainerFunctor.Notations.
Import Subset.Notations.

#[local] Generalizable Variables U T G A B C ϕ M.
#[local] Arguments ret T%function_scope {Return} {A}%type_scope _.

Import Kleisli.TraversableMonad.DerivedInstances.

(** * Theory of Traversable Monads *)
(**********************************************************************)
Section traversable_monad_theory.

  Context
    `{ret_inst: Return T}
    `{Map_T_inst: Map T}
    `{Traverse_T_inst: Traverse T}
    `{Bind_T_inst: Bind T T}
    `{Bindt_T_inst: Bindt T T}
    `{ToSubset_T_inst: ToSubset T}
    `{! Compat_Map_Bindt T T}
    `{! Compat_Traverse_Bindt T T}
    `{! Compat_Bind_Bindt T T}
    `{! Compat_ToSubset_Traverse T}.

  Context
    `{Map_U_inst: Map U}
    `{Traverse_U_inst: Traverse U}
    `{Bind_U_inst: Bind T U}
    `{Bindt_U_inst: Bindt T U}
    `{ToSubset_U_inst: ToSubset U}
    `{! Compat_Map_Bindt T U}
    `{! Compat_Traverse_Bindt T U}
    `{! Compat_Bind_Bindt T U}
    `{! Compat_ToSubset_Traverse U}.

  Context
    `{Monad_inst: ! TraversableMonad T}
    `{Module_inst: ! TraversableRightPreModule T U}.

  (** ** <<mapReduce>> on Traversble Monads *)
  (********************************************************************)
  Lemma mapReduce_bindt `{Applicative G} `{Monoid M}:
    forall `(g: B -> M) `(f: A -> G (T B)),
      map (mapReduce g) ∘ bindt (U := U) f =
        mapReduce (T := U) (map (mapReduce g) ∘ f).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (B : Type) (g : B -> M) (A : Type)
  (f : A -> G (T B)),
map (mapReduce g) ∘ bindt f =
mapReduce (map (mapReduce g) ∘ f)
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
forall (B : Type) (g : B -> M) (A : Type)
  (f : A -> G (T B)),
map (mapReduce g) ∘ bindt f =
mapReduce (map (mapReduce g) ∘ f)
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
map (mapReduce g) ∘ bindt f =
mapReduce (map (mapReduce g) ∘ f) unfold mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
map (traverse g) ∘ bindt f =
traverse (map (traverse g) ∘ f)
    rewrite (traverse_bindt (G1 := G) (G2 := const M) A B False).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt (map (traverse g) ∘ f) =
traverse (map (traverse g) ∘ f)
    rewrite 2(traverse_to_bindt).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt (map (bindt (map (ret T) ∘ g)) ∘ f) =
bindt
  (map (ret T) ∘ (map (bindt (map (ret T) ∘ g)) ∘ f))
    reassociate <- on right.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt (map (bindt (map (ret T) ∘ g)) ∘ f) =
bindt
  (map (ret T) ∘ map (bindt (map (ret T) ∘ g)) ∘ f)
    unfold_ops @Map_const.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt
  (map (bindt ((fun t : const M False => t) ∘ g)) ∘ f) =
bindt
  ((fun t : const (G M) False => t)
   ∘ map (bindt ((fun t : const M False => t) ∘ g))
   ∘ f)
    change (fun (x: ?A) => x) with (@id A).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt (map (bindt (id ∘ g)) ∘ f) =
bindt (id ∘ map (bindt (id ∘ g)) ∘ f)
    do 2 change (id ∘ ?f) with f.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
bindt (map (bindt g) ∘ f) = bindt (map (bindt g) ∘ f)
    fequal.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
Map_compose G (const M) =
(fun (X Y : Type) (_ : X -> Y) => id)
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
Mult_compose G (const M) = Mult_const
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
Map_compose G (const M) =
(fun (X Y : Type) (_ : X -> Y) => id) ext A' B' f'.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
f': A' -> B'
Map_compose G (const M) A' B' f' = id
      unfold Map_compose, Map_const, const.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
f': A' -> B'
map (map f') = id
      unfold map at 2.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
f': A' -> B'
map id = id
      now rewrite (fun_map_id (F := G)).
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
Mult_compose G (const M) = Mult_const ext A' B' [a b].
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
a: (G ∘ const M) A'
b: (G ∘ const M) B'
Mult_compose G (const M) A' B' (a, b) =
Mult_const A' B' (a, b)
      unfold Mult_compose, Mult_const.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
a: (G ∘ const M) A'
b: (G ∘ const M) B'
map mult (fst (a, b) ⊗ snd (a, b)) = a ● b
      unfold compose in *.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
a: G (const M A')
b: G (const M B')
map mult (fst (a, b) ⊗ snd (a, b)) = a ● b
      unfold const in *.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
a, b: G M
map mult (fst (a, b) ⊗ snd (a, b)) = a ● b
      cbn.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
B: Type
g: B -> M
A: Type
f: A -> G (T B)
A', B': Type
a, b: G M
map mult (a ⊗ b) = a ● b
      reflexivity.
  Qed.

  Lemma mapReduce_bind `{Monoid M}:
    forall `(g: B -> M) `(f: A -> T B),
      mapReduce g ∘ bind (U := U) f = mapReduce (mapReduce g ∘ f).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (B : Type) (g : B -> M) (A : Type)
  (f : A -> T B),
mapReduce g ∘ bind f = mapReduce (mapReduce g ∘ f)
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (B : Type) (g : B -> M) (A : Type)
  (f : A -> T B),
mapReduce g ∘ bind f = mapReduce (mapReduce g ∘ f)
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
B: Type
g: B -> M
A: Type
f: A -> T B
mapReduce g ∘ bind f = mapReduce (mapReduce g ∘ f) unfold mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
B: Type
g: B -> M
A: Type
f: A -> T B
traverse g ∘ bind f = traverse (traverse g ∘ f)
    rewrite (traverse_bind (G2 := const M) A B False).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
B: Type
g: B -> M
A: Type
f: A -> T B
bindt (traverse g ∘ f) = traverse (traverse g ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
B: Type
g: B -> M
A: Type
f: A -> T B
bindt (bindt (map (ret T) ∘ g) ∘ f) =
traverse (bindt (map (ret T) ∘ g) ∘ f)
    rewrite traverse_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
B: Type
g: B -> M
A: Type
f: A -> T B
bindt (bindt (map (ret T) ∘ g) ∘ f) =
bindt (map (ret T) ∘ (bindt (map (ret T) ∘ g) ∘ f))
    reflexivity.
  Qed.

  Lemma mapReduce_ret `{Monoid M}: forall `(f: A -> M),
      mapReduce f ∘ ret T = f.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f ∘ ret T = f
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (A : Type) (f : A -> M),
mapReduce f ∘ ret T = f
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
mapReduce f ∘ ret T = f unfold mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
traverse f ∘ ret T = f
    rewrite traverse_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
bindt (map (ret T) ∘ f) ∘ ret T = f
    rewrite (ktm_bindt0 (G := const M) A False).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
f: A -> M
map (ret T) ∘ f = f
    reflexivity.
  Qed.

  (** ** <<tolist>> on Traversable Monads *)
  (********************************************************************)
  Lemma tolist_ret: forall (A: Type),
      tolist ∘ ret T = ret list (A := A).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, tolist ∘ ret T = ret list
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, tolist ∘ ret T = ret list
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
tolist ∘ ret T = ret list
    unfold_ops @Tolist_Traverse.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
mapReduce (ret list) ∘ ret T = ret list
    now rewrite mapReduce_ret.
  Qed.

  Lemma tolist_bind: forall (A B: Type) (f: A -> T B),
      tolist ∘ bind f = bind (tolist ∘ f) ∘ tolist.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B),
tolist ∘ bind f = bind (tolist ∘ f) ∘ tolist
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B),
tolist ∘ bind f = bind (tolist ∘ f) ∘ tolist
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
tolist ∘ bind f = bind (tolist ∘ f) ∘ tolist
    unfold_ops @Tolist_Traverse.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (ret list) ∘ bind f =
bind (mapReduce (ret list) ∘ f) ∘ mapReduce (ret list)
    rewrite (mapReduce_bind (ret list) f).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret list) ∘ f) =
bind (mapReduce (ret list) ∘ f) ∘ mapReduce (ret list)
    rewrite (mapReduce_morphism (list A) (list B)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret list) ∘ f) =
mapReduce (bind (mapReduce (ret list) ∘ f) ∘ ret list)
    rewrite (kmon_bind0 (T := list)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret list) ∘ f) =
mapReduce (mapReduce (ret list) ∘ f)
    reflexivity.
  Qed.

  (** ** <<tosubset>> on Traversable Monads *)
  (********************************************************************)
  Lemma tosubset_hom1: forall (A: Type),
      tosubset ∘ ret T = ret subset (A := A).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, tosubset ∘ ret T = ret subset
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, tosubset ∘ ret T = ret subset
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
tosubset ∘ ret T = ret subset
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
mapReduce (ret subset) ∘ ret T = ret subset
    rewrite mapReduce_ret.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
ret subset = ret subset
    reflexivity.
  Qed.

  Lemma tosubset_hom2: forall (A B: Type) (f: A -> T B),
      tosubset ∘ bind (U := U) f = bind (tosubset ∘ f) ∘ tosubset.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B),
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B),
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (ret subset) ∘ bind f =
bind (tosubset ∘ f) ∘ tosubset
    rewrite mapReduce_bind.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret subset) ∘ f) =
bind (tosubset ∘ f) ∘ tosubset
    rewrite (tosubset_to_mapReduce (T := U)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret subset) ∘ f) =
bind (tosubset ∘ f) ∘ mapReduce (ret subset)
    rewrite (mapReduce_morphism (subset A) (subset B)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret subset) ∘ f) =
mapReduce (bind (tosubset ∘ f) ∘ ret subset)
    rewrite (kmon_bind0 (T := subset)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret subset) ∘ f) =
mapReduce (tosubset ∘ f)
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce (ret subset) ∘ f) =
mapReduce (mapReduce (ret subset) ∘ f)
    reflexivity.
  Qed.

  (** ** <<element_of>> on Traversable Monads *)
  (********************************************************************)
  Lemma element_of_hom1: forall (A: Type) (a: A),
      element_of a ∘ ret T = {{a}}.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A : Type) (a : A),
element_of a ∘ ret T = {{a}}
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A : Type) (a : A),
element_of a ∘ ret T = {{a}}
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a: A
element_of a ∘ ret T = {{a}}
    ext a'.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a, a': A
(element_of a ∘ ret T) a' = {{a}} a'
    unfold element_of, compose.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a, a': A
tosubset (ret T a') a = {{a}} a'
    compose near a' on left.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a, a': A
(tosubset ∘ ret T) a' a = {{a}} a'
    rewrite tosubset_hom1.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a, a': A
ret subset a' a = {{a}} a'
    cbv.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
a, a': A
(a' = a) = (a = a')
    now propext.
  Qed.

  Lemma element_of_hom2: forall (A B: Type) (f: A -> T B) (b: B),
      element_of b ∘ bind (U := U) f =
        mapReduce (op := Monoid_op_or) (unit := Monoid_unit_false)
          (mapReduce (op := Monoid_op_or) (unit := Monoid_unit_false)
             {{b}} ∘ f).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B) (b : B),
element_of b ∘ bind f =
mapReduce (mapReduce {{b}} ∘ f)
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B) (b : B),
element_of b ∘ bind f =
mapReduce (mapReduce {{b}} ∘ f)
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
b: B
element_of b ∘ bind f =
mapReduce (mapReduce {{b}} ∘ f)
    rewrite element_of_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
b: B
mapReduce {{b}} ∘ bind f =
mapReduce (mapReduce {{b}} ∘ f)
    rewrite mapReduce_bind.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
b: B
mapReduce (mapReduce {{b}} ∘ f) =
mapReduce (mapReduce {{b}} ∘ f)
    reflexivity.
  Qed.

End traversable_monad_theory.