From Tealeaves Require Export
  Classes.Multisorted.DecoratedTraversableMonad
  Classes.Multisorted.Theory.Container
  Classes.Multisorted.Theory.Targeted
  Adapters.KleisliToCoalgebraic.Multisorted.DTM.

Import ContainerFunctor.
Import Functors.List.

Import Subset.Notations.
Import TypeFamily.Notations.
Import Monoid.Notations.
Import Theory.Container.Notations.
Import List.ListNotations.
#[local] Open Scope list_scope.

#[local] Generalizable Variables A B C F G W T U K.

(** * Respectfulness Conditions for <<mbindd>> and Derived Operations *)
(**********************************************************************)

(** ** Identities for <<tolist>> and <<mapReduce>> *)
(**********************************************************************)
Section toBatchM.

  Context
    (U: Type -> Type)
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Lemma tolistmd_gen_to_runBatchM (fake: Type) `(t: U A):
    tolistmd_gen U fake t =
      runBatchM (F := const (list _))
        (fun k '(w, a) => [(w, (k, a))]) (toBatchM U fake t).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd_gen U fake t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd_gen U fake t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    unfold tolistmd_gen.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
mmapdt U (const (list (W * (K * A)))) tolistmd_gen_loc
  t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    rewrite mmapdt_to_runBatchM.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
runBatchM
  (fun k : K => map (mret T k) ∘ tolistmd_gen_loc k)
  (toBatchM U fake t) =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    reflexivity.
  Qed.

  Lemma tolistmd_to_runBatchM  (fake: Type) `(t: U A):
    tolistmd U t =
      runBatchM (fun k '(w, a) => [(w, (k, a))]) (toBatchM U fake t).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd U t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd U t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    unfold tolistmd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd_gen U False t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    rewrite (tolistmd_equiv U False fake).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistmd_gen U fake t =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    rewrite tolistmd_gen_to_runBatchM.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t) =
runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
  (toBatchM U fake t)
    reflexivity.
  Qed.

  Lemma tosetmd_to_runBatchM  (fake: Type) `(t: U A):
    tosetmd U t =
      runBatchM (F := (@const Type Type (subset (W * (K * A)))))
        (fun k '(w, a) => {{(w, (k, a))}}) (toBatchM U fake t).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tosetmd U t =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tosetmd U t =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
    unfold tosetmd, compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tosubset (tolistmd U t) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t) rewrite (tolistmd_to_runBatchM fake).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tosubset
  (runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
     (toBatchM U fake t)) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
    change (tosubset (F := list)
              (A := W * (K * A))) with
      (const (tosubset (A := W * (K * A))) (U fake)).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
const tosubset (U fake)
  (runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
     (toBatchM U fake t)) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
    cbn. (* <- needed for implicit arguments. *)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
const tosubset (U fake)
  (runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
     (toBatchM U fake t)) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
    rewrite (runBatchM_morphism (G1 := const (list (W * (K * A))))
               (G2 := const (subset (W * (K * A))))).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
runBatchM
  (fun k : K =>
   const tosubset (T k fake)
   ∘ (fun '(w, a) => [(w, (k, a))]))
  (toBatchM U fake t) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t)
    unfold compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
runBatchM
  (fun (k : K) (a : W * A) =>
   const tosubset (T k fake)
     (let '(w, a0) := a in [(w, (k, a0))]))
  (toBatchM U fake t) =
runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (toBatchM U fake t) fequal.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
(fun (k : K) (a : W * A) =>
 const tosubset (T k fake)
   (let '(w, a0) := a in [(w, (k, a0))])) =
(fun (k : K) '(w, a) => {{(w, (k, a))}}) ext k [w a].
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
k: K
w: W
a: A
const tosubset (T k fake) [(w, (k, a))] =
{{(w, (k, a))}}
    unfold const.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
k: K
w: W
a: A
tosubset [(w, (k, a))] = {{(w, (k, a))}}
    apply tosubset_list_one.
  Qed.

  Lemma tolistm_to_runBatchM (fake: Type) `(t: U A):
    tolistm U t =
      runBatchM (fun k '(w, a) => [(k, a)]) (toBatchM U fake t).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistm U t =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t)
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
tolistm U t =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t)
    unfold tolistm.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
(map extract ∘ tolistmd U) t =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t) unfold compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
map extract (tolistmd U t) =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t) rewrite (tolistmd_to_runBatchM fake).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
map extract
  (runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
     (toBatchM U fake t)) =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t)
    change (map (F := list) ?f) with (const (map (F := list) f) (U fake)).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
const (map extract) (U fake)
  (runBatchM (fun (k : K) '(w, a) => [(w, (k, a))])
     (toBatchM U fake t)) =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t)
    rewrite (runBatchM_morphism (G1 := const (list (W * (K * A))))
               (G2 := const (list (K * A)))
               (ψ := const (map (F := list) extract))).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
runBatchM
  (fun k : K =>
   const (map extract) (T k fake)
   ∘ (fun '(w, a) => [(w, (k, a))]))
  (toBatchM U fake t) =
runBatchM (fun (k : K) '(_, a) => [(k, a)])
  (toBatchM U fake t)
    fequal.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
fake, A: Type
t: U A
(fun k : K =>
 const (map extract) (T k fake)
 ∘ (fun '(w, a) => [(w, (k, a))])) =
(fun (k : K) '(_, a) => [(k, a)]) now ext k [w a].
  Qed.


End toBatchM.

(** ** Respectfulness for <<mbindd>> *)
(**********************************************************************)
Section mbindd_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Theorem mbindd_respectful:
    forall (A B: Type) (t: U A) (f g: forall k, W * A -> T k B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a))
      -> mbindd U f t = mbindd U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : W * A ~k~> T B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)) ->
mbindd U f t = mbindd U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : W * A ~k~> T B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)) ->
mbindd U f t = mbindd U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
mbindd U f t = mbindd U g t
    rewrite (tosetmd_to_runBatchM U B t) in hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
runBatchM
  (fun (k0 : K) '(w0, a0) => {{(w0, (k0, a0))}})
  (toBatchM U B t) (
  w, (k, a)) -> 
f k (w, a) = g k (w, a)
mbindd U f t = mbindd U g t
    rewrite mbindd_to_runBatchM.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
runBatchM
  (fun (k0 : K) '(w0, a0) => {{(w0, (k0, a0))}})
  (toBatchM U B t) (
  w, (k, a)) -> 
f k (w, a) = g k (w, a)
runBatchM f (toBatchM U B t) = mbindd U g t
    rewrite mbindd_to_runBatchM.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
runBatchM
  (fun (k0 : K) '(w0, a0) => {{(w0, (k0, a0))}})
  (toBatchM U B t) (
  w, (k, a)) -> 
f k (w, a) = g k (w, a)
runBatchM f (toBatchM U B t) =
runBatchM g (toBatchM U B t)
    induction (toBatchM U B t).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
c: C
hyp: forall (w : W) (k : K) (a : A),
runBatchM
  (fun (k0 : K) '(w0, a0) => {{(w0, (k0, a0))}})
  (Go c) (w, (k, a)) -> 
f k (w, a) = g k (w, a)
runBatchM f (Go c) = runBatchM g (Go c)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
p: W * A
hyp: forall (w : W) (k0 : K) (a : A),
runBatchM
  (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
  (Ap b p) (
  w, (k0, a)) -> 
f k0 (w, a) = g k0 (w, a)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
runBatchM f (Ap b p) = runBatchM g (Ap b p)
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
c: C
hyp: forall (w : W) (k : K) (a : A),
runBatchM
  (fun (k0 : K) '(w0, a0) => {{(w0, (k0, a0))}})
  (Go c) (w, (k, a)) -> 
f k (w, a) = g k (w, a)
runBatchM f (Go c) = runBatchM g (Go c) easy.
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
p: W * A
hyp: forall (w : W) (k0 : K) (a : A),
runBatchM
  (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
  (Ap b p) (
  w, (k0, a)) -> 
f k0 (w, a) = g k0 (w, a)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
runBatchM f (Ap b p) = runBatchM g (Ap b p) destruct p.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (Ap b (w, a)) (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
runBatchM f (Ap b (w, a)) = runBatchM g (Ap b (w, a))
      rewrite runBatchM_rw2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (Ap b (w, a)) (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
ap (fun A : Type => A) (runBatchM f b) (f k (w, a)) =
runBatchM g (Ap b (w, a))
      rewrite runBatchM_rw2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}})
  (Ap b (w, a)) (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
ap (fun A : Type => A) (runBatchM f b) (f k (w, a)) =
ap (fun A : Type => A) (runBatchM g b) (g k (w, a))
      rewrite runBatchM_rw2 in hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
ap (fun A : Type => A) (runBatchM f b) (f k (w, a)) =
ap (fun A : Type => A) (runBatchM g b) (g k (w, a))
      fequal.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
runBatchM f b = runBatchM g b
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
f k (w, a) = g k (w, a)
      +
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
runBatchM f b = runBatchM g b apply IHb.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
forall (w : W) (k0 : K) (a : A),
runBatchM (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
  b (w, (k0, a)) -> f k0 (w, a) = g k0 (w, a) intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
w0: W
k0: K
a0: A
H1: runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}}) b
  (w0, (k0, a0))
f k0 (w0, a0) = g k0 (w0, a0) apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
w0: W
k0: K
a0: A
H1: runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}}) b
  (w0, (k0, a0))
ap (const (W * (K * A) -> Prop))
  (runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
     b) {{(w, (k, a))}} (w0, (k0, a0))
        cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
w0: W
k0: K
a0: A
H1: runBatchM
  (fun (k : K) '(w, a) => {{(w, (k, a))}}) b
  (w0, (k0, a0))
(runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}}) b
 ● {{(w, (k, a))}}) (w0, (k0, a0)) now left.
      +
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
f k (w, a) = g k (w, a) apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: W * A ~k~> T B
C: Type
k: K
b: BatchM (T k B -> C)
w: W
a: A
hyp: forall (w0 : W) (k0 : K) (a0 : A),
ap (const (W * (K * A) -> Prop))
  (runBatchM
     (fun (k : K) '(w, a) => {{(w, (k, a))}}) b)
  {{(w, (k, a))}} (
  w0, (k0, a0)) -> 
f k0 (w0, a0) = g k0 (w0, a0)
IHb: (forall (w : W) (k0 : K) (a : A),
 runBatchM
   (fun (k : K) '(w0, a0) => {{(w0, (k, a0))}})
   b (w, (k0, a)) -> 
 f k0 (w, a) = g k0 (w, a)) ->
runBatchM f b = runBatchM g b
ap (const (W * (K * A) -> Prop))
  (runBatchM (fun (k : K) '(w, a) => {{(w, (k, a))}})
     b) {{(w, (k, a))}} (w, (k, a)) now right.
  Qed.

  (** *** For equalities with special cases *)
  (** Corollaries with conclusions of the form <<mbindd t = f t>> for
      other <<m*>> operations *)
  (********************************************************************)
  Corollary mbindd_respectful_mbind:
    forall (A B: Type) (t: U A) (f: forall k, W * A -> T k B) (g: forall k, A -> T k B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = g k a)
      -> mbindd U f t = mbind U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : A ~k~> T B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k a) ->
mbindd U f t = mbind U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : A ~k~> T B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k a) ->
mbindd U f t = mbind U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
mbindd U f t = mbind U g t rewrite mbind_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
mbindd U f t = mbindd U (g ◻ allK extract) t
    apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = (g ◻ allK extract) k (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = (g ◻ allK extract) k (w, a)
    unfold vec_compose, compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = g k (allK extract k (w, a)) cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: A ~k~> T B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = g k a auto.
  Qed.

  Corollary mbindd_respectful_mmapd:
    forall (A B: Type) (t: U A) (f: forall k, W * A -> T k B) (g: K -> W * A -> B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = mret T k (g k (w, a)))
      -> mbindd U f t = mmapd U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : K -> W * A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t ->
 f k (w, a) = mret T k (g k (w, a))) ->
mbindd U f t = mmapd U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : K -> W * A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t ->
 f k (w, a) = mret T k (g k (w, a))) ->
mbindd U f t = mmapd U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
mbindd U f t = mmapd U g t rewrite mmapd_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
mbindd U f t = mbindd U (mret T ◻ g) t
    apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = (mret T ◻ g) k (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = (mret T ◻ g) k (w, a)
    unfold vec_compose, compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = mret T k (g k (w, a)) cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = mret T k (g k (w, a)) auto.
  Qed.

  Corollary mbindd_respectful_mmap:
    forall (A B: Type) (t: U A) (f: forall k, W * A -> T k B) (g: K -> A -> B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = mret T k (g k a))
      -> mbindd U f t = mmap U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : K -> A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = mret T k (g k a)) ->
mbindd U f t = mmap U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : W * A ~k~> T B)
  (g : K -> A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = mret T k (g k a)) ->
mbindd U f t = mmap U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
mbindd U f t = mmap U g t rewrite mmap_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
mbindd U f t =
mbindd U ((mret T ◻ g) ◻ allK extract) t
    apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = ((mret T ◻ g) ◻ allK extract) k (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = ((mret T ◻ g) ◻ allK extract) k (w, a)
    unfold vec_compose, compose.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = mret T k (g k (allK extract k (w, a))) cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: W * A ~k~> T B
g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = mret T k (g k a)
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = mret T k (g k a) auto.
  Qed.

  Corollary mbindd_respectful_id:
    forall A (t: U A) (f: forall k, W * A -> T k A),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = mret T k a)
      -> mbindd U f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : W * A ~k~> T A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = mret T k a) ->
mbindd U f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : W * A ~k~> T A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = mret T k a) ->
mbindd U f t = t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: W * A ~k~> T A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a
mbindd U f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: W * A ~k~> T A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a
mbindd U f t = id t
    rewrite <- (mbindd_id U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: W * A ~k~> T A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a
mbindd U f t = mbindd U (mret T ◻ allK extract) t
    eapply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: W * A ~k~> T A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = (mret T ◻ allK extract) k (w, a)
    unfold vec_compose, compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: W * A ~k~> T A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = mret T k a auto.
  Qed.

End mbindd_respectful.

(** ** Respectfulness for <<mbindd>> *)
(**********************************************************************)
Section mbind_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Lemma mbind_respectful:
    forall (A B: Type) (t: U A) (f g: forall k, A -> T k B),
      (forall (k: K) (a: A),
          (k, a) ∈m t -> f k a = g k a)
      -> mbind U f t = mbind U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : A ~k~> T B),
(forall (k : K) (a : A), (k, a) ∈m t -> f k a = g k a) ->
mbind U f t = mbind U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : A ~k~> T B),
(forall (k : K) (a : A), (k, a) ∈m t -> f k a = g k a) ->
mbind U f t = mbind U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
mbind U f t = mbind U g t rewrite mbind_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
mbindd U (f ◻ allK extract) t = mbind U g t
    apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
(f ◻ allK extract) k (w, a) =
(g ◻ allK extract) k (w, a)
    introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
(f ◻ allK extract) k (w, a) =
(g ◻ allK extract) k (w, a)
    apply inmd_implies_in in premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
w: W
k: K
a: A
premise: (k, a) ∈m t
(f ◻ allK extract) k (w, a) =
(g ◻ allK extract) k (w, a)
    unfold vec_compose, compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: A ~k~> T B
hyp: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = g k a
w: W
k: K
a: A
premise: (k, a) ∈m t
f k a = g k a auto.
  Qed.

  (** *** For equalities with other operations *)
  (** Corollaries with conclusions of the form <<mbind t = f t>> for
      other <<m*>> operations *)
  (********************************************************************)
  Corollary mbind_respectful_mmapd:
    forall (A B: Type) (t: U A) (f: forall k, A -> T k B) (g: K -> W * A -> B),
      (forall (k: K) (w: W) (a: A),
          (w, (k, a)) ∈md t -> f k a = mret T k (g k (w, a)))
      -> mbind U f t = mmapd U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B)
  (g : K -> W * A -> B),
(forall (k : K) (w : W) (a : A),
 (w, (k, a)) ∈md t -> f k a = mret T k (g k (w, a))) ->
mbind U f t = mmapd U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B)
  (g : K -> W * A -> B),
(forall (k : K) (w : W) (a : A),
 (w, (k, a)) ∈md t -> f k a = mret T k (g k (w, a))) ->
mbind U f t = mmapd U g t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
mbind U f t = mmapd U g t rewrite mmapd_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
mbind U f t = mbindd U (mret T ◻ g) t
    symmetry.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
mbindd U (mret T ◻ g) t = mbind U f t apply mbindd_respectful_mbind.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> (mret T ◻ g) k (w, a) = f k a
    introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
(mret T ◻ g) k (w, a) = f k a symmetry.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k a = (mret T ◻ g) k (w, a)
    unfold vec_compose, compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> W * A -> B
H1: forall (k : K) (w : W) (a : A),
(w, (k, a)) ∈md t ->
f k a = mret T k (g k (w, a))
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k a = mret T k (g k (w, a)) auto.
  Qed.

  Corollary mbind_respectful_mmap:
    forall (A B: Type) (t: U A) (f: forall k, A -> T k B) (g: K -> A -> B),
      (forall (k: K) (a: A),
          (k, a) ∈m t -> f k a = mret T k (g k a))
      -> mbind U f t = mmap U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B)
  (g : K -> A -> B),
(forall (k : K) (a : A),
 (k, a) ∈m t -> f k a = mret T k (g k a)) ->
mbind U f t = mmap U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f : A ~k~> T B)
  (g : K -> A -> B),
(forall (k : K) (a : A),
 (k, a) ∈m t -> f k a = mret T k (g k a)) ->
mbind U f t = mmap U g t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
mbind U f t = mmap U g t rewrite mmap_to_mbind.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
mbind U f t = mbind U (mret T ◻ g) t
    symmetry.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
mbind U (mret T ◻ g) t = mbind U f t apply mbind_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
forall (k : K) (a : A),
(k, a) ∈m t -> (mret T ◻ g) k a = f k a
    introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
k: K
a: A
Hin: (k, a) ∈m t
(mret T ◻ g) k a = f k a symmetry.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
k: K
a: A
Hin: (k, a) ∈m t
f k a = (mret T ◻ g) k a
    unfold vec_compose, compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f: A ~k~> T B
g: K -> A -> B
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k (g k a)
k: K
a: A
Hin: (k, a) ∈m t
f k a = mret T k (g k a) auto.
  Qed.

  Corollary mbind_respectful_id: forall A (t: U A) (f: forall k, A -> T k A),
      (forall (k: K) (a: A),
          (k, a) ∈m t -> f k a = mret T k a)
      -> mbind U f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : A ~k~> T A),
(forall (k : K) (a : A),
 (k, a) ∈m t -> f k a = mret T k a) -> mbind U f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : A ~k~> T A),
(forall (k : K) (a : A),
 (k, a) ∈m t -> f k a = mret T k a) -> mbind U f t = t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: A ~k~> T A
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
mbind U f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: A ~k~> T A
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
mbind U f t = id t
    rewrite <- (mbind_id U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: A ~k~> T A
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
mbind U f t = mbind U (fun k : K => mret T k) t
    eapply mbind_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: A ~k~> T A
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
    unfold compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: A ~k~> T A
H1: forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a
forall (k : K) (a : A),
(k, a) ∈m t -> f k a = mret T k a auto.
  Qed.

End mbind_respectful.

(** ** Respectfulness for <<mmapd>> *)
(**********************************************************************)
Section mmapd_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Lemma mmapd_respectful:
    forall (A B: Type) (t: U A) (f g: K -> W * A -> B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a))
      -> mmapd U f t = mmapd U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : K -> W * A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)) ->
mmapd U f t = mmapd U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : K -> W * A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)) ->
mmapd U f t = mmapd U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
mmapd U f t = mmapd U g t do 2 rewrite mmapd_to_mbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
mbindd U (mret T ◻ f) t = mbindd U (mret T ◻ g) t
    apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
(mret T ◻ f) k (w, a) = (mret T ◻ g) k (w, a) introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
(mret T ◻ f) k (w, a) = (mret T ◻ g) k (w, a)
    unfold vec_compose, compose; cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
mret T k (f k (w, a)) = mret T k (g k (w, a)) fequal.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> W * A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
f k (w, a) = g k (w, a) auto.
  Qed.

  (** *** For equalities with other operations *)
  (** Corollaries with conclusions of the form <<mmapd t = f t>> for
      other <<m*>> operations *)
  (********************************************************************)
  Corollary mmapd_respectful_mmap:
    forall A (t: U A) (f: K -> W * A -> A) (g: K -> A -> A),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = g k a)
      -> mmapd U f t = mmap U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> W * A -> A)
  (g : K -> A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k a) ->
mmapd U f t = mmap U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> W * A -> A)
  (g : K -> A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = g k a) ->
mmapd U f t = mmap U g t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
g: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
mmapd U f t = mmap U g t rewrite mmap_to_mmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
g: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
mmapd U f t = mmapd U (g ◻ allK extract) t
    apply mmapd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
g: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = (g ◻ allK extract) k (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
g: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = g k a
w: W
k: K
a: A
Hin: (w, (k, a)) ∈md t
f k (w, a) = (g ◻ allK extract) k (w, a)
    unfold vec_compose, compose; cbn; auto.
  Qed.

  Corollary mmapd_respectful_id:
    forall (A: Type) (t: U A) (f: K -> W * A -> A),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k (w, a) = a)
      -> mmapd U f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> W * A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = a) ->
mmapd U f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> W * A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k (w, a) = a) ->
mmapd U f t = t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a
mmapd U f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a
mmapd U f t = id t
    rewrite <- (mmapd_id U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a
mmapd U f t = mmapd U (allK extract) t
    eapply mmapd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
f k (w, a) = allK extract k (w, a)
    cbn.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> W * A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k (w, a) = a auto.
  Qed.

End mmapd_respectful.

(** ** Respectfulness for <<mmap>> *)
(**********************************************************************)
Section mmap_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}.

  Lemma mmap_respectful:
    forall (A B: Type) (t: U A) (f g: K -> A -> B),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k a = g k a)
      -> mmap U f t = mmap U g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : K -> A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k a = g k a) ->
mmap U f t = mmap U g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A B : Type) (t : U A) (f g : K -> A -> B),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k a = g k a) ->
mmap U f t = mmap U g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = g k a
mmap U f t = mmap U g t do 2 rewrite mmap_to_mmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A, B: Type
t: U A
f, g: K -> A -> B
hyp: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = g k a
mmapd U (f ◻ allK extract) t =
mmapd U (g ◻ allK extract) t
    now apply mmapd_respectful.
  Qed.

  Corollary mmap_respectful_id:
    forall A (t: U A) (f: K -> A -> A),
      (forall (w: W) (k: K) (a: A),
          (w, (k, a)) ∈md t -> f k a = a)
      -> mmap U f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k a = a) -> mmap U f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
forall (A : Type) (t : U A) (f : K -> A -> A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> f k a = a) -> mmap U f t = t
    intros.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = a
mmap U f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = a
mmap U f t = id t
    rewrite <- (mmap_id U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = a
mmap U f t = mmap U (allK id) t
    eapply mmap_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f: K -> A -> A
H1: forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> f k a = allK id k a
    auto.
  Qed.

End mmap_respectful.

(** * Respectfulness for Targeted Operations *)
(**********************************************************************)

(** ** Respectfulness for <<kbindd>> *)
(**********************************************************************)
Section kbindd_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T} (j: K).

  Lemma kbindd_respectful:
    forall A (t: U A) (f g: W * A -> T j A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = g (w, a))
      -> kbindd U j f t = kbindd U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : W * A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g (w, a)) ->
kbindd U j f t = kbindd U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : W * A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g (w, a)) ->
kbindd U j f t = kbindd U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
kbindd U j f t = kbindd U j g t unfold kbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
mbindd U (btgd j f) t = mbindd U (btgd j g) t apply mbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
btgd j f k (w, a) = btgd j g k (w, a)
    introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
btgd j f k (w, a) = btgd j g k (w, a) compare values j and k.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: W * A -> T k A
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
btgd k f k (w, a) = btgd k g k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
btgd j f k (w, a) = btgd j g k (w, a)
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: W * A -> T k A
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
btgd k f k (w, a) = btgd k g k (w, a) do 2 rewrite btgd_eq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: W * A -> T k A
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
f (w, a) = g (w, a) auto.
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
btgd j f k (w, a) = btgd j g k (w, a) do 2 (rewrite btgd_neq; auto).
  Qed.

  (** *** For equalities with special cases *)
  (********************************************************************)
  Corollary kbindd_respectful_kbind:
    forall A (t: U A) (f: W * A -> T j A) (g: A -> T j A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = g a)
      -> kbindd U j f t = kbind U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g a) ->
kbindd U j f t = kbind U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g a) ->
kbindd U j f t = kbind U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
kbindd U j f t = kbind U j g t rewrite kbind_to_kbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
kbindd U j f t = kbindd U j (g ∘ extract) t
    apply kbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = (g ∘ extract) (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
w: W
a: A
Hin: (w, (j, a)) ∈md t
f (w, a) = (g ∘ extract) (w, a)
    apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
w: W
a: A
Hin: (w, (j, a)) ∈md t
(w, (j, a)) ∈md t auto.
  Qed.

  Corollary kbindd_respectful_kmapd:
    forall A (t: U A) (f: W * A -> T j A) (g: W * A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = mret T j (g (w, a)))
      -> kbindd U j f t = kmapd U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j (g (w, a))) ->
kbindd U j f t = kmapd U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j (g (w, a))) ->
kbindd U j f t = kmapd U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j (g (w, a))
kbindd U j f t = kmapd U j g t rewrite kmapd_to_kbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j (g (w, a))
kbindd U j f t = kbindd U j (mret T j ∘ g) t
    apply kbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j (g (w, a))
forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = (mret T j ∘ g) (w, a) introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j (g (w, a))
w: W
a: A
Hin: (w, (j, a)) ∈md t
f (w, a) = (mret T j ∘ g) (w, a)
    apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j (g (w, a))
w: W
a: A
Hin: (w, (j, a)) ∈md t
(w, (j, a)) ∈md t auto.
  Qed.

  Corollary kbindd_respectful_kmap:
    forall A (t: U A) (f: W * A -> T j A) (g: A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = mret T j (g a))
      -> kbindd U j f t = kmap U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)) ->
kbindd U j f t = kmap U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A)
  (g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)) ->
kbindd U j f t = kmap U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)
kbindd U j f t = kmap U j g t rewrite kmap_to_kmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)
kbindd U j f t = kmapd U j (g ∘ extract) t
    apply kbindd_respectful_kmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)
forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = mret T j ((g ∘ extract) (w, a))
    introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)
w: W
a: A
Hin: (w, (j, a)) ∈md t
f (w, a) = mret T j ((g ∘ extract) (w, a)) apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j (g a)
w: W
a: A
Hin: (w, (j, a)) ∈md t
(w, (j, a)) ∈md t auto.
  Qed.

  Corollary kbindd_respectful_id:
    forall A (t: U A) (f: W * A -> T j A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = mret T j a)
      -> kbindd U j f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j a) ->
kbindd U j f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> T j A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = mret T j a) ->
kbindd U j f t = t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j a
kbindd U j f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j a
kbindd U j f t = id t
    erewrite <- (kbindd_id U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j a
kbindd U j f t = kbindd U ?j (mret T ?j ∘ extract) t
    apply kbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> T j A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = mret T j a
forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
f (w, a) = (mret T j ∘ extract) (w, a)
    auto.
  Qed.

End kbindd_respectful.

(** ** Respectfulness for Heterogeneous Operations *)
(**********************************************************************)
Section mixed_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T} (j: K).

  Corollary kbind_respectful_kmapd:
    forall A (t: U A) (f: A -> T j A) (g: W * A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f a = mret T j (g (w, a)))
      -> kbind U j f t = kmapd U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A)
  (g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f a = mret T j (g (w, a))) ->
kbind U j f t = kmapd U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A)
  (g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f a = mret T j (g (w, a))) ->
kbind U j f t = kmapd U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
kbind U j f t = kmapd U j g t rewrite kmapd_to_kbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
kbind U j f t = kbindd U j (mret T j ∘ g) t
    rewrite kbind_to_kbindd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
kbindd U j (f ∘ extract) t =
kbindd U j (mret T j ∘ g) t apply kbindd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
forall (w : W) (a : A),
(w, (j, a)) ∈md t ->
(f ∘ extract) (w, a) = (mret T j ∘ g) (w, a)
    introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
w: W
a: A
Hin: (w, (j, a)) ∈md t
(f ∘ extract) (w, a) = (mret T j ∘ g) (w, a) apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = mret T j (g (w, a))
w: W
a: A
Hin: (w, (j, a)) ∈md t
(w, (j, a)) ∈md t auto.
  Qed.

End mixed_respectful.

(** ** Respectfulness for <<kbind>> *)
(**********************************************************************)
Section kbindd_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T} (j: K).

  Lemma kbind_respectful:
    forall A (t: U A) (f g: A -> T j A),
      (forall (a: A), (j, a) ∈m t -> f a = g a)
      -> kbind U j f t = kbind U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : A -> T j A),
(forall a : A, (j, a) ∈m t -> f a = g a) ->
kbind U j f t = kbind U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : A -> T j A),
(forall a : A, (j, a) ∈m t -> f a = g a) ->
kbind U j f t = kbind U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
kbind U j f t = kbind U j g t unfold kbind.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
mbind U (btg j f) t = mbind U (btg j g) t apply mbind_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
forall (k : K) (a : A),
(k, a) ∈m t -> btg j f k a = btg j g k a
    introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
k: K
a: A
premise: (k, a) ∈m t
btg j f k a = btg j g k a compare values j and k.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: A -> T k A
hyp: forall a : A, (k, a) ∈m t -> f a = g a
a: A
premise: (k, a) ∈m t
DESTR_EQs: k = k
btg k f k a = btg k g k a
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
k: K
a: A
premise: (k, a) ∈m t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
btg j f k a = btg j g k a
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: A -> T k A
hyp: forall a : A, (k, a) ∈m t -> f a = g a
a: A
premise: (k, a) ∈m t
DESTR_EQs: k = k
btg k f k a = btg k g k a do 2 rewrite btg_eq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
k: K
g, f: A -> T k A
hyp: forall a : A, (k, a) ∈m t -> f a = g a
a: A
premise: (k, a) ∈m t
DESTR_EQs: k = k
f a = g a auto.
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = g a
k: K
a: A
premise: (k, a) ∈m t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
btg j f k a = btg j g k a do 2 (rewrite btg_neq; auto).
  Qed.

  (** *** For equalities with special cases *)
  (********************************************************************)
  Corollary kbind_respectful_kmap:
    forall A (t: U A) (f: A -> T j A) (g: A -> A),
      (forall (a: A), (j, a) ∈m t -> f a = mret T j (g a))
      -> kbind U j f t = kmap U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A)
  (g : A -> A),
(forall a : A, (j, a) ∈m t -> f a = mret T j (g a)) ->
kbind U j f t = kmap U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A)
  (g : A -> A),
(forall a : A, (j, a) ∈m t -> f a = mret T j (g a)) ->
kbind U j f t = kmap U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: A -> A
hyp: forall a : A,
(j, a) ∈m t -> f a = mret T j (g a)
kbind U j f t = kmap U j g t rewrite kmap_to_kbind.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: A -> A
hyp: forall a : A,
(j, a) ∈m t -> f a = mret T j (g a)
kbind U j f t = kbind U j (mret T j ∘ g) t
    apply kbind_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: A -> A
hyp: forall a : A,
(j, a) ∈m t -> f a = mret T j (g a)
forall a : A, (j, a) ∈m t -> f a = (mret T j ∘ g) a
    introv Hin.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: A -> A
hyp: forall a : A,
(j, a) ∈m t -> f a = mret T j (g a)
a: A
Hin: (j, a) ∈m t
f a = (mret T j ∘ g) a apply hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
g: A -> A
hyp: forall a : A,
(j, a) ∈m t -> f a = mret T j (g a)
a: A
Hin: (j, a) ∈m t
(j, a) ∈m t auto.
  Qed.

  Corollary kbind_respectful_id:
    forall A (t: U A) (f: A -> T j A),
      (forall (a: A), (j, a) ∈m t -> f a = mret T j a)
      -> kbind U j f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A),
(forall a : A, (j, a) ∈m t -> f a = mret T j a) ->
kbind U j f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> T j A),
(forall a : A, (j, a) ∈m t -> f a = mret T j a) ->
kbind U j f t = t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = mret T j a
kbind U j f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = mret T j a
kbind U j f t = id t
    rewrite <- (kbind_id U (j := j)).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> T j A
hyp: forall a : A, (j, a) ∈m t -> f a = mret T j a
kbind U j f t = kbind U j (mret T j) t
    now apply kbind_respectful.
  Qed.

End kbindd_respectful.

(** ** Respectfulness for <<kmapd>> *)
(**********************************************************************)
Section kmapd_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T} (j: K).

  Lemma kmapd_respectful:
    forall A (t: U A) (f g: W * A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = g (w, a))
      -> kmapd U j f t = kmapd U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g (w, a)) ->
kmapd U j f t = kmapd U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g (w, a)) ->
kmapd U j f t = kmapd U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
kmapd U j f t = kmapd U j g t unfold kmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
mmapd U (tgtd j f) t = mmapd U (tgtd j g) t
    apply mmapd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t ->
tgtd j f k (w, a) = tgtd j g k (w, a) introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
tgtd j f k (w, a) = tgtd j g k (w, a)
    compare values j and k.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: W * A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
tgtd k f k (w, a) = tgtd k g k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
tgtd j f k (w, a) = tgtd j g k (w, a)
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: W * A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
tgtd k f k (w, a) = tgtd k g k (w, a) do 2 rewrite tgtd_eq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: W * A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f (w, a) = g (w, a)
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
f (w, a) = g (w, a) auto.
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g (w, a)
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
tgtd j f k (w, a) = tgtd j g k (w, a) do 2 (rewrite tgtd_neq; auto).
  Qed.

  (** *** For equalities with other operations *)
  (********************************************************************)
  Corollary kmapd_respectful_kmap:
    forall A (t: U A) (f: W * A -> A) (g: A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = g a)
      -> kmapd U j f t = kmap U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> A)
  (g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g a) ->
kmapd U j f t = kmap U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> A)
  (g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = g a) ->
kmapd U j f t = kmap U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
kmapd U j f t = kmap U j g t rewrite kmap_to_kmapd.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
kmapd U j f t = kmapd U j (g ∘ extract) t
    apply kmapd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = g a
forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = (g ∘ extract) (w, a) auto.
  Qed.

  Corollary kmapd_respectful_id: forall A (t: U A) (f: W * A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f (w, a) = a)
      -> kmapd U j f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = a) ->
kmapd U j f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : W * A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f (w, a) = a) ->
kmapd U j f t = t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = a
kmapd U j f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = a
kmapd U j f t = id t
    rewrite <- (kmapd_id (j := j) U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = a
kmapd U j f t = kmapd U j extract t
    apply kmapd_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: W * A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = a
forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f (w, a) = extract (w, a) auto.
  Qed.

End kmapd_respectful.

(** ** Respectfulness for <<kmap>> *)
(**********************************************************************)
Section kmap_respectful.

  Context
    {U: Type -> Type}
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T} (j: K).

  Lemma kmap_respectful:
    forall A (t: U A) (f g: A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f a = g a)
      -> kmap U j f t = kmap U j g t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f a = g a) ->
kmap U j f t = kmap U j g t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f g : A -> A),
(forall (w : W) (a : A),
 (w, (j, a)) ∈md t -> f a = g a) ->
kmap U j f t = kmap U j g t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
kmap U j f t = kmap U j g t unfold kmap.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
mmap U (tgt j f) t = mmap U (tgt j g) t apply mmap_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
forall (w : W) (k : K) (a : A),
(w, (k, a)) ∈md t -> tgt j f k a = tgt j g k a
    introv premise.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
tgt j f k a = tgt j g k a compare values j and k.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f a = g a
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
tgt k f k a = tgt k g k a
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
tgt j f k a = tgt j g k a
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f a = g a
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
tgt k f k a = tgt k g k a autorewrite with tea_tgt_eq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
A: Type
t: U A
f, g: A -> A
k: K
hyp: forall (w : W) (a : A),
(w, (k, a)) ∈md t -> f a = g a
w: W
a: A
premise: (w, (k, a)) ∈md t
DESTR_EQs: k = k
f a = g a eauto.
    -
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
tgt j f k a = tgt j g k a autorewrite with tea_tgt_neq.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f, g: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = g a
w: W
k: K
a: A
premise: (w, (k, a)) ∈md t
DESTR_NEQ: j <> k
DESTR_NEQs: k <> j
id a = id a auto.
  Qed.

  Corollary kmap_respectful_id:
    forall A (t: U A) (f: A -> A),
      (forall (w: W) (a: A),
          (w, (j, a)) ∈md t -> f a = a)
      -> kmap U j f t = t.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> A),
(forall (w : W) (a : A), (w, (j, a)) ∈md t -> f a = a) ->
kmap U j f t = t
  Proof.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
forall (A : Type) (t : U A) (f : A -> A),
(forall (w : W) (a : A), (w, (j, a)) ∈md t -> f a = a) ->
kmap U j f t = t
    introv hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = a
kmap U j f t = t change t with (id t) at 2.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = a
kmap U j f t = id t
    rewrite <- (kmap_id (j := j) U).
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = a
kmap U j f t = kmap U j id t
    apply kmap_respectful.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  W T
j: K
A: Type
t: U A
f: A -> A
hyp: forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = a
forall (w : W) (a : A),
(w, (j, a)) ∈md t -> f a = id a auto.
  Qed.

End kmap_respectful.