From Tealeaves Require Export
  Classes.Kleisli.Theory.DecoratedContainerFunctor
  Classes.Kleisli.DecoratedContainerMonad.

Import Monoid.Notations.
Import Functor.Notations.
Import Subset.Notations.
Import List.ListNotations.
Import ContainerFunctor.Notations.
Import DecoratedContainerFunctor.Notations.

#[local] Generalizable Variables A T U W.


(** * Basic properties of containers *)
(**********************************************************************)
Section decorated_container_monad_theory.

  Context
    `{op: Monoid_op W}
    `{unit: Monoid_unit W}.

  Context
    `{ret_inst: Return T}
    `{Bindd_T_inst: Bindd W T T}
    `{Mapd_T_inst: Mapd W T}
    `{Bind_T_inst: Bind T T}
    `{Map_T_inst: Map T}
    `{Map_Bindd_T_inst: ! Compat_Map_Bindd W T T}
    `{Bind_Bindd_T_inst: ! Compat_Bind_Bindd W T T}
    `{Mapd_Bindd_T_inst: ! Compat_Mapd_Bindd W T T}.

  Context
    `{ToCtxset_T_inst: ToCtxset W T}
    `{ToSubset_T_inst: ToSubset T}
    `{! Compat_ToSubset_ToCtxset W T}
    `{! DecoratedContainerMonad W T}.

  Context
    `{Mapd_U_inst: Mapd W U}
    `{Bind_U_inst: Bind T U}
    `{Map_U_inst: Map U}
    `{Bindd_U_inst: Bindd W T U}
    `{Map_Bindd_inst: ! Compat_Map_Bindd W T U}
    `{Bind_Bindd_inst: ! Compat_Bind_Bindd W T U}
    `{Mapd_Bindd_inst: ! Compat_Mapd_Bindd W T U}.

  Context
    `{ToCtxset_U_inst: ToCtxset W U}
    `{ToSubset_U_inst: ToSubset U}
    `{! Compat_ToSubset_ToCtxset W U}
    `{Module_inst: ! DecoratedContainerRightModule W T U}.

  Variables (A B: Type).

  Implicit Types (t: U A) (b: B) (w: W) (a: A).

  Lemma dconm_morphism_ret: forall (A: Type),
      toctxset ∘ ret (T := T) (A := A) =
        ret (T := ctxset W).
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall A : Type, toctxset ∘ ret = ret
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall A : Type, toctxset ∘ ret = ret
    apply kdm_hom_ret.
  Qed.

  Lemma dconm_morphism_bind: forall (A B: Type) (f: W * A -> T B),
      toctxset ∘ bindd (U := U) f =
        bindd (U := ctxset W) (toctxset ∘ f) ∘ toctxset (F := U).
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (f : W * A -> T B),
toctxset ∘ bindd f = bindd (toctxset ∘ f) ∘ toctxset
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (f : W * A -> T B),
toctxset ∘ bindd f = bindd (toctxset ∘ f) ∘ toctxset
    apply kdmod_parhom_bind.
  Qed.

  Section ind_spec.

    Theorem ind_ret_iff: forall {A: Type} (w: W) (a1 a2: A),
        (w, a1) ∈d ret (T := T) a2 <-> w = Ƶ /\ a1 = a2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A : Type) w (a1 a2 : A),
(w, a1) ∈d ret a2 <-> w = Ƶ /\ a1 = a2
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A : Type) w (a1 a2 : A),
(w, a1) ∈d ret a2 <-> w = Ƶ /\ a1 = a2
      intros.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
(w, a1) ∈d ret a2 <-> w = Ƶ /\ a1 = a2
      compose near a2 on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
(element_ctx_of (w, a1) ∘ ret) a2 <-> w = Ƶ /\ a1 = a2
      rewrite element_ctx_of_toctxset.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
(evalAt (w, a1) ∘ toctxset ∘ ret) a2 <->
w = Ƶ /\ a1 = a2
      reassociate -> on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
(evalAt (w, a1) ∘ (toctxset ∘ ret)) a2 <->
w = Ƶ /\ a1 = a2
      rewrite (kdm_hom_ret (ϕ := @toctxset W T _)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
(evalAt (w, a1) ∘ ret) a2 <-> w = Ƶ /\ a1 = a2
      unfold evalAt, compose;
        unfold_ops @Return_ctxset.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
w: W
a1, a2: A0
a2 = a1 /\ w = Ƶ <-> w = Ƶ /\ a1 = a2
      intuition.
    Qed.

    Theorem ind_bindd_iff: forall w t f b,
        (w, b) ∈d bindd (U := U) f t <->
          exists (wa: W) (a: A), (wa, a) ∈d t /\
                              exists wb: W, (wb, b) ∈d f (wa, a) /\
                                         w = wa ● wb.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : W * A -> T B) b,
(w, b) ∈d bindd f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : W * A -> T B) b,
(w, b) ∈d bindd f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      introv.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: W * A -> T B
b: B
(w, b) ∈d bindd f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      compose near t on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: W * A -> T B
b: B
(element_ctx_of (w, b) ∘ bindd f) t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      rewrite element_ctx_of_toctxset.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: W * A -> T B
b: B
(evalAt (w, b) ∘ toctxset ∘ bindd f) t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      reassociate -> on left.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: W * A -> T B
b: B
(evalAt (w, b) ∘ (toctxset ∘ bindd f)) t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      rewrite (kdmod_parhom_bind (ϕ := @toctxset W U _)).
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: W * A -> T B
b: B
(evalAt (w, b) ∘ (bindd (toctxset ∘ f) ∘ toctxset)) t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ w = wa ● wb))
      reflexivity.
    Qed.

    Theorem ind_bindd_iff':
      forall `(f: W * A -> T B) (t: U A) (wtotal: W) (b: B),
        (wtotal, b) ∈d bindd f t <->
          exists (w1 w2: W) (a: A),
            (w1, a) ∈d t /\ (w2, b) ∈d f (w1, a)
            /\ wtotal = w1 ● w2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (f : W * A -> T B) t (wtotal : W) b,
(wtotal, b) ∈d bindd f t <->
(exists w1 w2 a,
   (w1, a) ∈d t /\
   (w2, b) ∈d f (w1, a) /\ wtotal = w1 ● w2)
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (f : W * A -> T B) t (wtotal : W) b,
(wtotal, b) ∈d bindd f t <->
(exists w1 w2 a,
   (w1, a) ∈d t /\
   (w2, b) ∈d f (w1, a) /\ wtotal = w1 ● w2)
      intros.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
f: W * A -> T B
t: U A
wtotal: W
b: B
(wtotal, b) ∈d bindd f t <->
(exists w1 w2 a,
   (w1, a) ∈d t /\
   (w2, b) ∈d f (w1, a) /\ wtotal = w1 ● w2)
      rewrite ind_bindd_iff.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
f: W * A -> T B
t: U A
wtotal: W
b: B
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W,
      (wb, b) ∈d f (wa, a) /\ wtotal = wa ● wb)) <->
(exists w1 w2 a,
   (w1, a) ∈d t /\
   (w2, b) ∈d f (w1, a) /\ wtotal = w1 ● w2)
      splits; intros ?; preprocess;
        (repeat eexists); eauto.
    Qed.

    Corollary ind_bind_iff: forall w t f b,
        (w, b) ∈d bind f t <->
          exists (wa: W) (a: A),
            (wa, a) ∈d t /\
              exists wb: W, (wb, b) ∈d f a /\
                         w = wa ● wb.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : A -> T B) b,
(w, b) ∈d bind f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb))
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : A -> T B) b,
(w, b) ∈d bind f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb))
      introv.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: A -> T B
b: B
(w, b) ∈d bind f t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb))
      rewrite bind_to_bindd.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: A -> T B
b: B
(w, b) ∈d bindd (f ∘ extract) t <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb))
      rewrite ind_bindd_iff.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: A -> T B
b: B
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W,
      (wb, b) ∈d (f ∘ extract) (wa, a) /\ w = wa ● wb)) <->
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb))
      reflexivity.
    Qed.

    Corollary ind_bind_iff': forall w t f b,
        (w, b) ∈d bind f t <->
          exists (wa wb: W) (a: A),
            (wa, a) ∈d t /\
              (wb, b) ∈d f a /\
              w = wa ● wb.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : A -> T B) b,
(w, b) ∈d bind f t <->
(exists (wa wb : W) a,
   (wa, a) ∈d t /\ (wb, b) ∈d f a /\ w = wa ● wb)
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall w t (f : A -> T B) b,
(w, b) ∈d bind f t <->
(exists (wa wb : W) a,
   (wa, a) ∈d t /\ (wb, b) ∈d f a /\ w = wa ● wb)
      introv.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: A -> T B
b: B
(w, b) ∈d bind f t <->
(exists (wa wb : W) a,
   (wa, a) ∈d t /\ (wb, b) ∈d f a /\ w = wa ● wb)
      rewrite ind_bind_iff.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
w: W
t: U A
f: A -> T B
b: B
(exists (wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f a /\ w = wa ● wb)) <->
(exists (wa wb : W) a,
   (wa, a) ∈d t /\ (wb, b) ∈d f a /\ w = wa ● wb)
      splits; intros ?; preprocess;
        (repeat eexists); eauto.
    Qed.

    Corollary in_bindd_iff: forall t f b,
        b ∈ bindd (U := U) f t <->
          exists (wa: W) (a: A),
            (wa, a) ∈d t /\ b ∈ f (wa, a).
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall t (f : W * A -> T B) b,
b ∈ bindd f t <->
(exists (wa : W) a, (wa, a) ∈d t /\ b ∈ f (wa, a))
    Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall t (f : W * A -> T B) b,
b ∈ bindd f t <->
(exists (wa : W) a, (wa, a) ∈d t /\ b ∈ f (wa, a))
      introv.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
b ∈ bindd f t <->
(exists (wa : W) a, (wa, a) ∈d t /\ b ∈ f (wa, a))
      rewrite ind_iff_in.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists e : W, (e, b) ∈d bindd f t) <->
(exists (wa : W) a, (wa, a) ∈d t /\ b ∈ f (wa, a))
      setoid_rewrite ind_bindd_iff.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (e wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)) <->
(exists (wa : W) a, (wa, a) ∈d t /\ b ∈ f (wa, a))
      setoid_rewrite ind_iff_in.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (e wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)) <->
(exists (wa : W) a,
   (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a)))
      split.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (e wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)) ->
exists (wa : W) a,
  (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a))
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (wa : W) a,
   (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a))) ->
exists (e wa : W) a,
  (wa, a) ∈d t /\
  (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)
      -
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (e wa : W) a,
   (wa, a) ∈d t /\
   (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)) ->
exists (wa : W) a,
  (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a)) intros [w [wa [a [Hin [wb [Hin' Heq]]]]]].
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
w, wa: W
a: A
Hin: (wa, a) ∈d t
wb: W
Hin': (wb, b) ∈d f (wa, a)
Heq: w = wa ● wb
exists (wa : W) a,
  (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a))
        eauto.
      -
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
(exists (wa : W) a,
   (wa, a) ∈d t /\ (exists e : W, (e, b) ∈d f (wa, a))) ->
exists (e wa : W) a,
  (wa, a) ∈d t /\
  (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb) intros [wa [a [Hin [w rest]]]].
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
wa: W
a: A
Hin: (wa, a) ∈d t
w: W
rest: (w, b) ∈d f (wa, a)
exists (e wa : W) a,
  (wa, a) ∈d t /\
  (exists wb : W, (wb, b) ∈d f (wa, a) /\ e = wa ● wb)
        exists (wa ● w) wa a.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
t: U A
f: W * A -> T B
b: B
wa: W
a: A
Hin: (wa, a) ∈d t
w: W
rest: (w, b) ∈d f (wa, a)
(wa, a) ∈d t /\
(exists wb : W,
   (wb, b) ∈d f (wa, a) /\ wa ● w = wa ● wb) eauto.
    Qed.

  End ind_spec.

  (*******************************************************************)
  Corollary bindd_respectful:
    forall A B (t: U A) (f: W * A -> T B) (g: W * A -> T B),
      (forall (w: W) (a: A), (w, a) ∈d t -> f (w, a) = g (w, a))
      -> bindd f t = bindd g t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f g : W * A -> T B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = g (w, a)) ->
bindd f t = bindd g t
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f g : W * A -> T B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = g (w, a)) ->
bindd f t = bindd g t
    introv hyp.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f, g: W * A0 -> T B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = g (w, a)
bindd f t = bindd g t
    apply dconmod_pointwise.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f, g: W * A0 -> T B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = g (w, a)
forall (e : W) (a : A0),
(e, a) ∈d t -> f (e, a) = g (e, a)
    assumption.
  Qed.

  Corollary bindd_respectful_bind:
    forall A B (t: U A) (f: W * A -> T B) (g: A -> T B),
      (forall (w: W) (a: A), (w, a) ∈d t -> f (w, a) = g a)
      -> bindd f t = bind g t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : A -> T B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = g a) ->
bindd f t = bind g t
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : A -> T B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = g a) ->
bindd f t = bind g t
    introv hyp.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> T B0
hyp: forall w (a : A0), (w, a) ∈d t -> f (w, a) = g a
bindd f t = bind g t
    rewrite bind_to_bindd.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> T B0
hyp: forall w (a : A0), (w, a) ∈d t -> f (w, a) = g a
bindd f t = bindd (g ∘ extract) t
    apply bindd_respectful.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> T B0
hyp: forall w (a : A0), (w, a) ∈d t -> f (w, a) = g a
forall w (a : A0),
(w, a) ∈d t -> f (w, a) = (g ∘ extract) (w, a)
    introv Hin.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> T B0
hyp: forall w (a : A0), (w, a) ∈d t -> f (w, a) = g a
w: W
a: A0
Hin: (w, a) ∈d t
f (w, a) = (g ∘ extract) (w, a)
    eauto.
  Qed.

  Corollary bindd_respectful_mapd:
    forall A B (t: U A) (f: W * A -> T B) (g: W * A -> B),
      (forall (w: W) (a: A), (w, a) ∈d t -> f (w, a) = ret (g (w, a)))
      -> bindd f t = mapd g t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : W * A -> B),
(forall w (a : A),
 (w, a) ∈d t -> f (w, a) = ret (g (w, a))) ->
bindd f t = mapd g t
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : W * A -> B),
(forall w (a : A),
 (w, a) ∈d t -> f (w, a) = ret (g (w, a))) ->
bindd f t = mapd g t
    introv hyp.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: W * A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g (w, a))
bindd f t = mapd g t
    rewrite mapd_to_bindd.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: W * A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g (w, a))
bindd f t = bindd (ret ∘ g) t
    apply bindd_respectful.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: W * A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g (w, a))
forall w (a : A0),
(w, a) ∈d t -> f (w, a) = (ret ∘ g) (w, a)
    assumption.
  Qed.

  Corollary bindd_respectful_map:
    forall A B (t: U A) (f: W * A -> T B) (g: A -> B),
      (forall (w: W) (a: A), (w, a) ∈d t -> f (w, a) = ret (g a))
      -> bindd f t = map g t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : A -> B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = ret (g a)) ->
bindd f t = map g t
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A B : Type) (t : U A) (f : W * A -> T B)
  (g : A -> B),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = ret (g a)) ->
bindd f t = map g t
    introv hyp.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g a)
bindd f t = map g t
    rewrite map_to_bindd.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g a)
bindd f t = bindd (ret ∘ g ∘ extract) t
    apply bindd_respectful.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0, B0: Type
t: U A0
f: W * A0 -> T B0
g: A0 -> B0
hyp: forall w (a : A0),
(w, a) ∈d t -> f (w, a) = ret (g a)
forall w (a : A0),
(w, a) ∈d t -> f (w, a) = (ret ∘ g ∘ extract) (w, a)
    assumption.
  Qed.

  Corollary bindd_respectful_id:
    forall A (t: U A) (f: W * A -> T A),
      (forall (w: W) (a: A), (w, a) ∈d t -> f (w, a) = ret a)
      -> bindd f t = t.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A : Type) (t : U A) (f : W * A -> T A),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = ret a) ->
bindd f t = t
  Proof.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B: Type
forall (A : Type) (t : U A) (f : W * A -> T A),
(forall w (a : A), (w, a) ∈d t -> f (w, a) = ret a) ->
bindd f t = t
    intros.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
t: U A0
f: W * A0 -> T A0
H: forall w (a : A0), (w, a) ∈d t -> f (w, a) = ret a
bindd f t = t change t with (id t) at 2.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
t: U A0
f: W * A0 -> T A0
H: forall w (a : A0), (w, a) ∈d t -> f (w, a) = ret a
bindd f t = id t
    rewrite <- kdmod_bindd1.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
t: U A0
f: W * A0 -> T A0
H: forall w (a : A0), (w, a) ∈d t -> f (w, a) = ret a
bindd f t = bindd (ret ∘ extract) t
    eapply bindd_respectful.
W: Type
op: Monoid_op W
unit: Monoid_unit W
T: Type -> Type
ret_inst: Return T
Bindd_T_inst: Bindd W T T
Mapd_T_inst: Mapd W T
Bind_T_inst: Bind T T
Map_T_inst: Map T
Map_Bindd_T_inst: Compat_Map_Bindd W T T
Bind_Bindd_T_inst: Compat_Bind_Bindd W T T
Mapd_Bindd_T_inst: Compat_Mapd_Bindd W T T
ToCtxset_T_inst: ToCtxset W T
ToSubset_T_inst: ToSubset T
Compat_ToSubset_ToCtxset0: Compat_ToSubset_ToCtxset W
  T
DecoratedContainerMonad0: DecoratedContainerMonad W T
U: Type -> Type
Mapd_U_inst: Mapd W U
Bind_U_inst: Bind T U
Map_U_inst: Map U
Bindd_U_inst: Bindd W T U
Map_Bindd_inst: Compat_Map_Bindd W T U
Bind_Bindd_inst: Compat_Bind_Bindd W T U
Mapd_Bindd_inst: Compat_Mapd_Bindd W T U
ToCtxset_U_inst: ToCtxset W U
ToSubset_U_inst: ToSubset U
Compat_ToSubset_ToCtxset1: Compat_ToSubset_ToCtxset W
  U
Module_inst: DecoratedContainerRightModule W T U
A, B, A0: Type
t: U A0
f: W * A0 -> T A0
H: forall w (a : A0), (w, a) ∈d t -> f (w, a) = ret a
forall w (a : A0),
(w, a) ∈d t -> f (w, a) = (ret ∘ extract) (w, a)
    eauto.
  Qed.

End decorated_container_monad_theory.


(** ** Instance for <<env>> *) (* TODO *)
(**********************************************************************)
(*
#[export] Instance DecoratedContainerMonad_env `{Monoid W}:
  DecoratedContainerMonad W (env W).
Proof.
  constructor.
  - admit.
  - intros. ext l. unfold compose.
    induction l as [| [w a] rest IHrest].
    + cbn. unfold_ops @ToCtxset_env.
      autorewrite with tea_list.
      rewrite bindd_ctxset_nil.
      reflexivity.
    + change (bindd f ((w, a) :: rest)) with
        (shift list (w, f (w, a)) ++ bindd f rest).
      cbn.
      unfold_ops @ToCtxset_env.
      autorewrite with tea_list.
      change (tosubset (A := W * ?A)) with
        (toctxset (F := env W) (A := A)).
      rewrite bindd_ctxset_add.
      rewrite bindd_ctxset_one.
      rewrite <- IHrest.
      fequal.
      rewrite (DecoratedFunctor.shift_spec). 2:admit.
      compose near (f (w, a)).
      rewrite (fun_map_map).
Abort.

 *)