Foldmap.v

 From Tealeaves Require Import
   Classes.Multisorted.DecoratedTraversableMonad
   Classes.Multisorted.Theory.Container
   Classes.Multisorted.Theory.Targeted
   Functors.List
   Functors.Subset
   Functors.Constant.

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

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

(** * Foldmap *)
(******************************************************************************)

(** ** Operations *)
(******************************************************************************)
Section foldmap.

  Context
    (U : Type -> Type)
    `{MultiDecoratedTraversablePreModule W T U}
    `{! MultiDecoratedTraversableMonad W T}
    `{M_mn_op: Monoid_op M}
    `{M_mn_unit: Monoid_unit M}.

  Definition mapReducemd_gen {A} (fake: Type) (f : K -> (W * A) -> M): U A -> M :=
    mmapdt (B := fake) U (const M) f.

  Definition mapReducemd {A} (f : K -> (W * A) -> M): U A -> M :=
    mapReducemd_gen False f.

  Definition mapReducem {A} (f : K -> A -> M) : U A -> M :=
    mapReducemd (f ◻ allK (extract (W := (prod W)))).

  Definition mapReducekd {A} (k: K) (f : W * A -> M): U A -> M :=
    mapReducemd (tgt_def k f (const Ƶ)).

  Definition mapReducek {A} (k: K) (f : A -> M): U A -> M :=
    mapReducem (tgt_def k f (const Ƶ)).

  Lemma mapReducemd_to_mmapdt {A} (f : K -> (W * A) -> M):
    mapReducemd f = mmapdt (B := False) U (const M) f.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
A: Type
f: K -> W * A -> M
mapReducemd f = mmapdt U (const M) f
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
A: Type
f: K -> W * A -> M
mapReducemd f = mmapdt U (const M) f
    reflexivity.
  Qed.

  Lemma mapReducem_to_mapReducemd {A} (f : K -> A -> M):
    mapReducem f = mapReducemd (f ◻ allK (extract (W := (prod W)))).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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
A: Type
f: K -> A -> M
mapReducem f = mapReducemd (f ◻ allK extract)
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
A: Type
f: K -> A -> M
mapReducem f = mapReducemd (f ◻ allK extract)
    reflexivity.
  Qed.

  Lemma mapReducemd_fake `{! Monoid M}: forall {A} (fake1 fake2: Type),
      mapReducemd_gen (A := A) fake1 = mapReducemd_gen fake2.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
forall A fake1 fake2 : Type,
mapReducemd_gen fake1 = mapReducemd_gen fake2
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
forall A fake1 fake2 : Type,
mapReducemd_gen fake1 = mapReducemd_gen fake2
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A, fake1, fake2: Type
mapReducemd_gen fake1 = mapReducemd_gen fake2
    ext f.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A, fake1, fake2: Type
f: K -> W * A -> M
mapReducemd_gen fake1 f = mapReducemd_gen fake2 f
    unfold mapReducemd_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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A, fake1, fake2: Type
f: K -> W * A -> M
mmapdt U (const M) f = mmapdt U (const M) f
    unfold mmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A, fake1, fake2: Type
f: K -> W * A -> M
mbinddt U (const M) (mapMret ◻ f) =
mbinddt U (const M) (mapMret ◻ f)
    rewrite (mbinddt_constant_applicative2 U fake1 fake2).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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A, fake1, fake2: Type
f: K -> W * A -> M
mbinddt U (const M) (mapMret ◻ f) =
mbinddt U (const M) (mapMret ◻ f)
    reflexivity.
  Qed.

  Lemma mapReducekd_to_kmapdt `{! Monoid M} {A} (f : W * A -> M) {k: K}:
    mapReducekd k f = kmapdt U k (G := const M) f.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = kmapdt U k f
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = kmapdt U k f
    unfold kmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = mmapdt U (const M) (tgtdt k f)
    unfold mapReducekd, mapReducemd.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducemd_gen False (tgt_def k f (const Ƶ)) =
mmapdt U (const M) (tgtdt k f)
    rewrite (mapReducemd_fake False 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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducemd_gen A (tgt_def k f (const Ƶ)) =
mmapdt U (const M) (tgtdt k f)
    unfold mapReducemd_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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mmapdt U (const M) (tgt_def k f (const Ƶ)) =
mmapdt U (const M) (tgtdt k f)
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
tgt_def k f (const Ƶ) = tgtdt k f
    ext j [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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k, j: K
w: W
a: A
tgt_def k f (const Ƶ) j (w, a) = tgtdt k f j (w, a)
    unfold tgt_def, tgtdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k, j: K
w: W
a: A
(if k == j then f else const Ƶ) (w, a) =
(if k == j then f (w, a) else pure a)
    destruct_eq_args k j.
  Qed.

  Lemma mapReducek_to_kmapt `{! Monoid M} {A} (f : A -> M) {k: K}:
    mapReducek k f = ktraverse U k (G := const M) f.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducek k f = ktraverse U k f
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducek k f = ktraverse U k f
    unfold mapReducek, mapReducem, mapReducemd.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducemd_gen False
  (tgt_def k f (const Ƶ) ◻ allK extract) =
ktraverse U k f
    rewrite (mapReducemd_fake False 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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducemd_gen A
  (tgt_def k f (const Ƶ) ◻ allK extract) =
ktraverse U k f
    reflexivity.
  Qed.

  Lemma mapReducekd_to_mapReducemd `{! Monoid M} {A} (f : W * A -> M) {k: K}:
    mapReducekd k f = mapReducemd (tgt_def (A := W * A) k f (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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = mapReducemd (tgt_def k f (const Ƶ))
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = mapReducemd (tgt_def k f (const Ƶ))
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapReducekd k f = mapReducemd (tgt_def k f (const Ƶ))
    rewrite mapReducekd_to_kmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
kmapdt U k f = mapReducemd (tgt_def k f (const Ƶ))
    rewrite kmapdt_to_mmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mmapdt U (const M) (tgtdt k f) =
mapReducemd (tgt_def k f (const Ƶ))
    rewrite mapReducemd_to_mmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mmapdt U (const M) (tgtdt k f) =
mmapdt U (const M) (tgt_def k f (const Ƶ))
    unfold mmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mbinddt U (const M) (mapMret ◻ tgtdt k f) =
mbinddt U (const M) (mapMret ◻ tgt_def k f (const Ƶ))
    rewrite (mbinddt_constant_applicative2 U A False).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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mbinddt U (const M) (mapMret ◻ tgtdt k f) =
mbinddt U (const M) (mapMret ◻ tgt_def k f (const Ƶ))
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
mapMret ◻ tgtdt k f = mapMret ◻ tgt_def k f (const Ƶ) 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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k: K
tgtdt k f = tgt_def k f (const Ƶ) ext j [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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k, j: K
w: W
a: A
tgtdt k f j (w, a) = tgt_def k f (const Ƶ) j (w, a)
    unfold tgtdt, tgt_def.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: W * A -> M
k, j: K
w: W
a: A
(if k == j then f (w, a) else pure a) =
(if k == j then f else const Ƶ) (w, a)
    destruct_eq_args k j.
  Qed.

  Lemma mapReducek_to_mapReducekd `{! Monoid M} {A} (f : A -> M) {k: K}:
    mapReducek k f = mapReducekd k (f ∘ extract (W := prod W)).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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducek k f = mapReducekd k (f ∘ extract)
  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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducek k f = mapReducekd k (f ∘ extract)
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mapReducek k f = mapReducekd k (f ∘ extract)
    rewrite mapReducek_to_kmapt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
ktraverse U k f = mapReducekd k (f ∘ extract)
    unfold ktraverse.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mmapt U (const M) (tgtt k f) =
mapReducekd k (f ∘ extract)
    rewrite mapReducekd_to_kmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mmapt U (const M) (tgtt k f) =
kmapdt U k (f ∘ extract)
    unfold mmapt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mmapdt U (const M) (tgtt k f ◻ allK extract) =
kmapdt U k (f ∘ extract)
    unfold kmapdt.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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
mmapdt U (const M) (tgtt k f ◻ allK extract) =
mmapdt U (const M) (tgtdt k (f ∘ extract))
    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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k: K
tgtt k f ◻ allK extract = tgtdt k (f ∘ extract) (ext j [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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k, j: K
w: W
a: A
(tgtt k f ◻ allK extract) j (w, a) =
tgtdt k (f ∘ extract) j (w, a)
    unfold tgtt, tgtdt, 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
M: Type
M_mn_op: Monoid_op M
M_mn_unit: Monoid_unit M
Monoid0: Monoid M
A: Type
f: A -> M
k, j: K
w: W
a: A
(if k == j then f else pure) (allK extract j (w, a)) =
(if k == j then f (extract (w, a)) else pure a)
    destruct_eq_args k j.
  Qed.

End foldmap.

Section tolist_and_tosubset.

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

  Lemma tolistmd_gen_to_mapReducemd_gen : forall {A} {fake:Type} (t: U A),
      tolistmd_gen U fake t = mapReducemd_gen U fake tolistmd_gen_loc 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 fake : Type) (t : U A),
tolistmd_gen U fake t =
mapReducemd_gen U fake tolistmd_gen_loc 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 fake : Type) (t : U A),
tolistmd_gen U fake t =
mapReducemd_gen U fake tolistmd_gen_loc t
    reflexivity.
  Qed.

  Lemma tolistmd_to_mapReducemd : forall {A},
      tolistmd (A := A) (T := T) U = mapReducemd U tolistmd_gen_loc.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,
tolistmd U = mapReducemd U tolistmd_gen_loc
  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,
tolistmd U = mapReducemd U tolistmd_gen_loc
    reflexivity.
  Qed.

  Definition tosetmd_gen_loc {A}: K -> W * A -> subset (W * (K * A)) :=
    fun k '(w, a) => {{ (w, (k, a)) }}.

  Lemma tosetmd_to_mapReducemd : forall {A},
      tosetmd (A := A) (T := T) U = mapReducemd U tosetmd_gen_loc.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,
tosetmd U = mapReducemd U tosetmd_gen_loc
  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,
tosetmd U = mapReducemd U tosetmd_gen_loc
    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
tosetmd U = mapReducemd U tosetmd_gen_loc
    unfold tosetmd.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
ContainerFunctor.tosubset ∘ tolistmd U =
mapReducemd U tosetmd_gen_loc
    rewrite tolistmd_to_mapReducemd.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
ContainerFunctor.tosubset
∘ mapReducemd U tolistmd_gen_loc =
mapReducemd U tosetmd_gen_loc
    unfold mapReducemd, mapReducemd_gen, mmapdt.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
ContainerFunctor.tosubset
∘ mbinddt U (const (list (W * (K * A))))
    (mapMret ◻ tolistmd_gen_loc) =
mbinddt U (const (W * (K * A) -> Prop))
  (mapMret ◻ tosetmd_gen_loc)
    change (ContainerFunctor.tosubset (A := (W * (K * A))))
      with (const (ContainerFunctor.tosubset (A := (W * (K * A))))
              (list (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
A: Type
const ContainerFunctor.tosubset (list (W * (K * A)))
∘ mbinddt U (const (list (W * (K * A))))
    (mapMret ◻ tolistmd_gen_loc) =
mbinddt U (const (W * (K * A) -> Prop))
  (mapMret ◻ tosetmd_gen_loc)
    Set Keyed Unification.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
const ContainerFunctor.tosubset (list (W * (K * A)))
∘ mbinddt U (const (list (W * (K * A))))
    (mapMret ◻ tolistmd_gen_loc) =
mbinddt U (const (W * (K * A) -> Prop))
  (mapMret ◻ tosetmd_gen_loc)
    rewrite (dtp_mbinddt_morphism W T U
                 (const (list (W * (K * A))))
                 (const (subset (W * (K * A))))
                 (H6 := ApplicativeMorphism_monoid_morphism)).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
mbinddt U (const (W * (K * A) -> Prop))
  ((fun k : K =>
    const
      (fun (l : list (W * (K * A))) (a : W * (K * A))
       =>
       (fix In
          (a0 : W * (K * A)) (l0 : list (W * (K * A)))
          {struct l0} : Prop :=
          match l0 with
          | [] => False
          | b :: m => b = a0 \/ In a0 m
          end) a l) (T k False))
   ◻ (mapMret ◻ tolistmd_gen_loc)) =
mbinddt U (const (W * (K * A) -> Prop))
  (mapMret ◻ tosetmd_gen_loc)
    Unset Keyed Unification.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
mbinddt U (const (W * (K * A) -> Prop))
  ((fun k : K =>
    const
      (fun (l : list (W * (K * A))) (a : W * (K * A))
       =>
       (fix In
          (a0 : W * (K * A)) (l0 : list (W * (K * A)))
          {struct l0} : Prop :=
          match l0 with
          | [] => False
          | b :: m => b = a0 \/ In a0 m
          end) a l) (T k False))
   ◻ (mapMret ◻ tolistmd_gen_loc)) =
mbinddt U (const (W * (K * A) -> Prop))
  (mapMret ◻ tosetmd_gen_loc)
    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: Type
(fun k : K =>
 const
   (fun (l : list (W * (K * A))) (a : W * (K * A)) =>
    (fix In
       (a0 : W * (K * A)) (l0 : list (W * (K * A)))
       {struct l0} : Prop :=
       match l0 with
       | [] => False
       | b :: m => b = a0 \/ In a0 m
       end) a l) (T k False))
◻ (mapMret ◻ tolistmd_gen_loc) =
mapMret ◻ tosetmd_gen_loc
    ext j (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
j: K
w: W
a: A
((fun k : K =>
  const
    (fun (l : list (W * (K * A))) (a : W * (K * A)) =>
     (fix In
        (a0 : W * (K * A)) (l0 : list (W * (K * A)))
        {struct l0} : Prop :=
        match l0 with
        | [] => False
        | b :: m => b = a0 \/ In a0 m
        end) a l) (T k False))
 ◻ (mapMret ◻ tolistmd_gen_loc)) j (w, a) =
(mapMret ◻ tosetmd_gen_loc) j (w, a)
    ext (j', (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
j: K
w: W
a: A
j': W
w': K
a': A
((fun k : K =>
  const
    (fun (l : list (W * (K * A))) (a : W * (K * A)) =>
     (fix In
        (a0 : W * (K * A)) (l0 : list (W * (K * A)))
        {struct l0} : Prop :=
        match l0 with
        | [] => False
        | b :: m => b = a0 \/ In a0 m
        end) a l) (T k False))
 ◻ (mapMret ◻ tolistmd_gen_loc)) j (w, a)
  (j', (w', a')) =
(mapMret ◻ tosetmd_gen_loc) j (w, a) (j', (w', a'))
    unfold vec_compose, compose, mapMret, vec_apply, 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
A: Type
j: K
w: W
a: A
j': W
w': K
a': A
(fix In
   (a : W * (K * A)) (l : list (W * (K * A))) {struct
    l} : Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
   end) (j', (w', a'))
  (map (mret T j) (tolistmd_gen_loc j (w, a))) =
map (mret T j) (tosetmd_gen_loc j (w, a))
  (j', (w', a'))
    unfold_ops @Map_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
A: Type
j: K
w: W
a: A
j': W
w': K
a': A
(fix In
   (a : W * (K * A)) (l : list (W * (K * A))) {struct
    l} : Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
   end) (j', (w', a')) (tolistmd_gen_loc j (w, a)) =
tosetmd_gen_loc j (w, a) (j', (w', a'))
    unfold tosetmd_gen_loc,
      tolistmd_gen_loc.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
j: K
w: W
a: A
j': W
w': K
a': A
((w, (j, a)) = (j', (w', a')) \/ False) =
{{(w, (j, a))}} (j', (w', a'))
    propext; intuition.
  Qed.

  #[global] Instance ApplicativeMorphism_filterk : forall {A} (k: K),
      ApplicativeMorphism (const (list (W * (K * A))))
                          (const (list (W * A)))
                          (const (filterk 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
forall (A : Type) (k : K),
ApplicativeMorphism (const (list (W * (K * A))))
  (const (list (W * A))) (const (filterk k))
  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) (k : K),
ApplicativeMorphism (const (list (W * (K * A))))
  (const (list (W * A))) (const (filterk k))
    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
k: K
ApplicativeMorphism (const (list (W * (K * A))))
  (const (list (W * A))) (const (filterk k)) eapply ApplicativeMorphism_monoid_morphism.
    Unshelve.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
k: K
Monoid_Morphism (list (W * (K * A))) (list (W * A))
  (filterk k) constructor; try typeclasses 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
A: Type
k: K
filterk 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
k: K
forall a1 a2 : list (W * (K * A)),
filterk k (a1 ● a2) = filterk k a1 ● filterk k a2
    -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
k: K
filterk k Ƶ = Ƶ 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: Type
k: K
forall a1 a2 : list (W * (K * A)),
filterk k (a1 ● a2) = filterk k a1 ● filterk k a2 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
k: K
a1, a2: list (W * (K * A))
filterk k (a1 ● a2) = filterk k a1 ● filterk k a2 apply filterk_app.
  Qed.

  Lemma toklistd_to_mapReducekd : forall {A} (k: K),
      toklistd (T := T) (A := A) U k = mapReducekd U k (fun p => [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
forall (A : Type) (k : K),
toklistd U k = mapReducekd U k (fun p : W * A => [p])
    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) (k : K),
toklistd U k = mapReducekd U k (fun p : W * A => [p])
      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
k: K
toklistd U k = mapReducekd U k (fun p : W * A => [p])
      unfold toklistd.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
k: K
filterk k ∘ tolistmd U =
mapReducekd U k (fun p : W * A => [p])
      rewrite tolistmd_to_mapReducemd.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
k: K
filterk k ∘ mapReducemd U tolistmd_gen_loc =
mapReducekd U k (fun p : W * A => [p])
      unfold mapReducemd, mapReducemd_gen, mmapdt.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
k: K
filterk k
∘ mbinddt U (const (list (W * (K * A))))
    (mapMret ◻ tolistmd_gen_loc) =
mapReducekd U k (fun p : W * A => [p])
      rewrite (dtp_mbinddt_morphism W T U
                 (const (list (W * (K * A))))
                 (const (list (W * A)))
                 (H6 := ApplicativeMorphism_filterk 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
k: K
mbinddt U (const (list (W * A)))
  ((fun k0 : K => const (filterk k) (T k0 False))
   ◻ (mapMret ◻ tolistmd_gen_loc)) =
mapReducekd U k (fun p : W * A => [p])
      unfold mapReducekd, mapReducemd, mapReducemd_gen, mmapdt.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
k: K
mbinddt U (const (list (W * A)))
  ((fun k0 : K => const (filterk k) (T k0 False))
   ◻ (mapMret ◻ tolistmd_gen_loc)) =
mbinddt U (const (list (W * A)))
  (mapMret
   ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))
      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: Type
k: K
(fun k0 : K => const (filterk k) (T k0 False))
◻ (mapMret ◻ tolistmd_gen_loc) =
mapMret ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ) ext j (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
k, j: K
w: W
a: A
((fun k0 : K => const (filterk k) (T k0 False))
 ◻ (mapMret ◻ tolistmd_gen_loc)) j (w, a) =
(mapMret ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))
  j (w, a)
      unfold vec_compose, compose, mapMret, vec_apply, tgt_def.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
k, j: K
w: W
a: A
const (filterk k) (T j False)
  (map (mret T j) (tolistmd_gen_loc j (w, a))) =
map (mret T j)
  ((if k == j then fun p : W * A => [p] else const Ƶ)
     (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
k, j: K
w: W
a: A
(if k == j then [(w, a)] else []) =
map (mret T j)
  ((if k == j then fun p : W * A => [p] else const Ƶ)
     (w, a)) destruct_eq_args k j.
    Qed.

  Lemma toksetd_to_mapReducekd : forall {A} (t: U A) (k : K),
      toksetd U k t = mapReducekd U k (fun p => {{p}}) 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) (k : K),
toksetd U k t =
mapReducekd U k (fun p : W * A => {{p}}) 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) (k : K),
toksetd U k t =
mapReducekd U k (fun p : W * A => {{p}}) 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
k: K
toksetd U k t =
mapReducekd U k (fun p : W * A => {{p}}) t
    unfold toksetd.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
(ContainerFunctor.tosubset ∘ toklistd U k) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    rewrite toklistd_to_mapReducekd.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
(ContainerFunctor.tosubset
 ∘ mapReducekd U k (fun p : W * A => [p])) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    unfold mapReducemd, mapReducemd_gen, mmapdt.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
(ContainerFunctor.tosubset
 ∘ mapReducekd U k (fun p : W * A => [p])) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    change (ContainerFunctor.tosubset (A := (W * A)))
      with (const (ContainerFunctor.tosubset (A := (W * A)))
              (list (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
(const ContainerFunctor.tosubset (list (W * A))
 ∘ mapReducekd U k (fun p : W * A => [p])) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    Set Keyed Unification.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
(const ContainerFunctor.tosubset (list (W * A))
 ∘ mapReducekd U k (fun p : W * A => [p])) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    rewrite (dtp_mbinddt_morphism W T U
               (const (list (W * A)))
               (const (subset (W * A)))
               (H6 := ApplicativeMorphism_monoid_morphism)).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
mbinddt U (const (W * A -> Prop))
  ((fun k : K =>
    const
      (fun (l : list (W * A)) (a : W * A) =>
       (fix In
          (a0 : W * A) (l0 : list (W * A)) {struct l0} :
            Prop :=
          match l0 with
          | [] => False
          | b :: m => b = a0 \/ In a0 m
          end) a l) (T k False))
   ◻ (mapMret
      ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    Unset Keyed Unification.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
mbinddt U (const (W * A -> Prop))
  ((fun k : K =>
    const
      (fun (l : list (W * A)) (a : W * A) =>
       (fix In
          (a0 : W * A) (l0 : list (W * A)) {struct l0} :
            Prop :=
          match l0 with
          | [] => False
          | b :: m => b = a0 \/ In a0 m
          end) a l) (T k False))
   ◻ (mapMret
      ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))) t =
mapReducekd U k (fun p : W * A => {{p}}) t
    unfold mapReducekd, mapReducemd, mapReducemd_gen, mmapdt.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
mbinddt U (const (W * A -> Prop))
  ((fun k : K =>
    const
      (fun (l : list (W * A)) (a : W * A) =>
       (fix In
          (a0 : W * A) (l0 : list (W * A)) {struct l0} :
            Prop :=
          match l0 with
          | [] => False
          | b :: m => b = a0 \/ In a0 m
          end) a l) (T k False))
   ◻ (mapMret
      ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))) t =
mbinddt U (const (W * A -> Prop))
  (mapMret
   ◻ tgt_def k (fun p : W * A => {{p}}) (const Ƶ)) 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
A: Type
t: U A
k: K
(fun k : K =>
 const
   (fun (l : list (W * A)) (a : W * A) =>
    (fix In
       (a0 : W * A) (l0 : list (W * A)) {struct l0} :
         Prop :=
       match l0 with
       | [] => False
       | b :: m => b = a0 \/ In a0 m
       end) a l) (T k False))
◻ (mapMret
   ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ)) =
mapMret ◻ tgt_def k (fun p : W * A => {{p}}) (const Ƶ)
    ext j (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, j: K
w: W
a: A
((fun k : K =>
  const
    (fun (l : list (W * A)) (a : W * A) =>
     (fix In
        (a0 : W * A) (l0 : list (W * A)) {struct l0} :
          Prop :=
        match l0 with
        | [] => False
        | b :: m => b = a0 \/ In a0 m
        end) a l) (T k False))
 ◻ (mapMret
    ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))) j
  (w, a) =
(mapMret
 ◻ tgt_def k (fun p : W * A => {{p}}) (const Ƶ)) j
  (w, a)
    ext (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, j: K
w: W
a: A
w': W
a': A
((fun k : K =>
  const
    (fun (l : list (W * A)) (a : W * A) =>
     (fix In
        (a0 : W * A) (l0 : list (W * A)) {struct l0} :
          Prop :=
        match l0 with
        | [] => False
        | b :: m => b = a0 \/ In a0 m
        end) a l) (T k False))
 ◻ (mapMret
    ◻ tgt_def k (fun p : W * A => [p]) (const Ƶ))) j
  (w, a) (w', a') =
(mapMret
 ◻ tgt_def k (fun p : W * A => {{p}}) (const Ƶ)) j
  (w, a) (w', a')
    unfold vec_compose, compose, mapMret, vec_apply, 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
A: Type
t: U A
k, j: K
w: W
a: A
w': W
a': A
(fix In (a : W * A) (l : list (W * A)) {struct l} :
     Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
   end) (w', a')
  (map (mret T j)
     (tgt_def k (fun p : W * A => [p])
        (fun _ : W * A => Ƶ) j (w, a))) =
map (mret T j)
  (tgt_def k (fun p : W * A => {{p}})
     (fun _ : W * A => Ƶ) j (w, a)) (w', a')
    unfold_ops @Map_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
A: Type
t: U A
k, j: K
w: W
a: A
w': W
a': A
(fix In (a : W * A) (l : list (W * A)) {struct l} :
     Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
   end) (w', a')
  (tgt_def k (fun p : W * A => [p])
     (fun _ : W * A => Ƶ) j (w, a)) =
tgt_def k (fun p : W * A => {{p}})
  (fun _ : W * A => Ƶ) j (w, a) (w', a')
    unfold tgt_def.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, j: K
w: W
a: A
w': W
a': A
(fix In (a : W * A) (l : list (W * A)) {struct l} :
     Prop :=
   match l with
   | [] => False
   | b :: m => b = a \/ In a m
   end) (w', a')
  ((if k == j
    then fun p : W * A => [p]
    else fun _ : W * A => Ƶ) (w, a)) =
(if k == j
 then fun p : W * A => {{p}}
 else fun _ : W * A => Ƶ) (w, a) (w', a')
    propext; destruct_eq_args k j; intuition.
  Qed.

End tolist_and_tosubset.

Section morphisms.

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

  Generalizable Variables ϕ.

  Lemma mapReducemd_morphism:
    forall {A}
      `{Monoid M1} `{Monoid M2}
      `{! Monoid_Morphism M1 M2 ϕ} (f: K -> W * A -> M1),
      ϕ ∘ mapReducemd U f = mapReducemd U (fun k => ϕ ∘ f 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
forall (A M1 : Type) (op : Monoid_op M1)
  (unit0 : Monoid_unit M1),
Monoid M1 ->
forall (M2 : Type) (op0 : Monoid_op M2)
  (unit1 : Monoid_unit M2),
Monoid M2 ->
forall ϕ : M1 -> M2,
Monoid_Morphism M1 M2 ϕ ->
forall f : K -> W * A -> M1,
ϕ ∘ mapReducemd U f = mapReducemd U (compose ϕ ○ f)
  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 M1 : Type) (op : Monoid_op M1)
  (unit0 : Monoid_unit M1),
Monoid M1 ->
forall (M2 : Type) (op0 : Monoid_op M2)
  (unit1 : Monoid_unit M2),
Monoid M2 ->
forall ϕ : M1 -> M2,
Monoid_Morphism M1 M2 ϕ ->
forall f : K -> W * A -> M1,
ϕ ∘ mapReducemd U f = mapReducemd U (compose ϕ ○ f)
    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, M1: Type
op: Monoid_op M1
unit0: Monoid_unit M1
H1: Monoid M1
M2: Type
op0: Monoid_op M2
unit1: Monoid_unit M2
H2: Monoid M2
ϕ: M1 -> M2
Monoid_Morphism0: Monoid_Morphism M1 M2 ϕ
f: K -> W * A -> M1
ϕ ∘ mapReducemd U f = mapReducemd U (compose ϕ ○ f)
    change ϕ with (const ϕ (U False)).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, M1: Type
op: Monoid_op M1
unit0: Monoid_unit M1
H1: Monoid M1
M2: Type
op0: Monoid_op M2
unit1: Monoid_unit M2
H2: Monoid M2
ϕ: M1 -> M2
Monoid_Morphism0: Monoid_Morphism M1 M2 ϕ
f: K -> W * A -> M1
const ϕ (U False) ∘ mapReducemd U f =
mapReducemd U (compose (const ϕ (U False)) ○ f)
    unfold mapReducemd, mapReducemd_gen, mmapdt.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, M1: Type
op: Monoid_op M1
unit0: Monoid_unit M1
H1: Monoid M1
M2: Type
op0: Monoid_op M2
unit1: Monoid_unit M2
H2: Monoid M2
ϕ: M1 -> M2
Monoid_Morphism0: Monoid_Morphism M1 M2 ϕ
f: K -> W * A -> M1
const ϕ (U False) ∘ mbinddt U (const M1) (mapMret ◻ f) =
mbinddt U (const M2)
  (mapMret ◻ compose (const ϕ (U False)) ○ f)
    rewrite (dtp_mbinddt_morphism W T U
               (A := A)
               (B := False)
               (ix := ix)
               (ϕ := const ϕ)
               (const M1)
               (const M2)
               (H6 := ApplicativeMorphism_monoid_morphism)).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, M1: Type
op: Monoid_op M1
unit0: Monoid_unit M1
H1: Monoid M1
M2: Type
op0: Monoid_op M2
unit1: Monoid_unit M2
H2: Monoid M2
ϕ: M1 -> M2
Monoid_Morphism0: Monoid_Morphism M1 M2 ϕ
f: K -> W * A -> M1
mbinddt U (const M2)
  ((fun k : K => const ϕ (T k False)) ◻ (mapMret ◻ f)) =
mbinddt U (const M2)
  (mapMret ◻ compose (const ϕ (U False)) ○ f)
    reflexivity.
  Qed.

  Lemma mapReducemd_through_tolist {A} `{Monoid M} (f : K -> (W * A) -> M):
    mapReducemd U f = mapReduce_list (fun '(w, (k, a)) => f k (w, a)) ∘ tolistmd 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, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
mapReducemd U f =
mapReduce_list (fun '(w, (k, a)) => f k (w, a))
∘ tolistmd U
  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
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
mapReducemd U f =
mapReduce_list (fun '(w, (k, a)) => f k (w, a))
∘ tolistmd U
    rewrite tolistmd_to_mapReducemd.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, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
mapReducemd U f =
mapReduce_list (fun '(w, (k, a)) => f k (w, a))
∘ mapReducemd U tolistmd_gen_loc
    rewrite mapReducemd_morphism.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, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
mapReducemd U f =
mapReducemd U
  (compose
     (mapReduce_list
        (fun '(w, (k0, a)) => f k0 (w, a)))
   ○ tolistmd_gen_loc)
    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, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
f =
compose
  (mapReduce_list (fun '(w, (k0, a)) => f k0 (w, a)))
○ tolistmd_gen_loc 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
A, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
k: K
w: W
a: A
f k (w, a) =
(mapReduce_list (fun '(w, (k, a)) => f k (w, a))
 ∘ tolistmd_gen_loc 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, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
f: K -> W * A -> M
k: K
w: W
a: A
f k (w, a) = f k (w, a) ● Ƶ
    now simpl_monoid.
  Qed.

End morphisms.

Section forall_and_exists.

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

  Definition Forallmd {A} (P: K -> W * A -> Prop) :=
    mapReducemd U (T := T)
      (M_mn_op := Monoid_op_and) (M_mn_unit := Monoid_unit_true) P.

  Definition Forallkd {A} (k: K) (P: W * A -> Prop) :=
    mapReducekd U k (T := T)
      (M_mn_op := Monoid_op_and) (M_mn_unit := Monoid_unit_true) P.

  Lemma Forallmd_to_mapReducemd {A} (P: K -> W * A -> Prop ):
    Forallmd P =
    mapReducemd U (T := T)
      (M_mn_op := Monoid_op_and) (M_mn_unit := Monoid_unit_true) 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: Type
P: K -> W * A -> Prop
Forallmd P = mapReducemd U P
  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
A: Type
P: K -> W * A -> Prop
Forallmd P = mapReducemd U P
    reflexivity.
  Qed.

  Lemma Forallkd_to_mapReducekd {A} (k: K) (P: W * A -> Prop):
    Forallkd k P =
    mapReducekd U k (T := T)
      (M_mn_op := Monoid_op_and) (M_mn_unit := Monoid_unit_true) 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: Type
k: K
P: W * A -> Prop
Forallkd k P = mapReducekd U k P
  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
A: Type
k: K
P: W * A -> Prop
Forallkd k P = mapReducekd U k P
    reflexivity.
  Qed.

  Lemma Forallkd_to_Forallmd {A} (k: K) (P: W * A -> Prop):
    Forallkd k P =
      Forallmd (tgt_def k P (const True)).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
k: K
P: W * A -> Prop
Forallkd k P = Forallmd (tgt_def k P (const True))
  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
A: Type
k: K
P: W * A -> Prop
Forallkd k P = Forallmd (tgt_def k P (const True))
    unfold Forallkd, Forallmd.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
k: K
P: W * A -> Prop
mapReducekd U k P =
mapReducemd U (tgt_def k P (const True))
    unfold mapReducekd.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
k: K
P: W * A -> Prop
mapReducemd U (tgt_def k P (const Ƶ)) =
mapReducemd U (tgt_def k P (const True))
    reflexivity.
  Qed.

  Definition Forallmd_spec : forall {A} (P: W * (K * A) -> Prop) (t: U A),
      (forall w k a, (w, (k, a)) ∈md t -> P (w, (k, a))) =
        Forallmd (fun k '(w, a) => P (w, (k, a))) 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) (P : W * (K * A) -> Prop) (t : U A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> P (w, (k, a))) =
Forallmd (fun (k : K) '(w, a) => P (w, (k, a))) 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) (P : W * (K * A) -> Prop) (t : U A),
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> P (w, (k, a))) =
Forallmd (fun (k : K) '(w, a) => P (w, (k, a))) 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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> P (w, (k, a))) =
Forallmd (fun (k : K) '(w, a) => P (w, (k, a))) t
    unfold Forallmd.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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 (w, (k, a)) ∈md t -> P (w, (k, a))) =
mapReducemd U (fun (k : K) '(w, a) => P (w, (k, a))) t
    unfold tosetmd.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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 (ContainerFunctor.tosubset ∘ tolistmd U) t
   (w, (k, a)) -> P (w, (k, a))) =
mapReducemd U (fun (k : K) '(w, a) => P (w, (k, a))) t
    rewrite (mapReducemd_through_tolist 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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 (ContainerFunctor.tosubset ∘ tolistmd U) t
   (w, (k, a)) -> P (w, (k, a))) =
(mapReduce_list (fun '(w, (k, a)) => P (w, (k, a)))
 ∘ tolistmd U) 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
A: Type
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset (tolistmd U t) (w, (k, a)) ->
 P (w, (k, a))) =
mapReduce_list (fun '(w, (k, a)) => P (w, (k, a)))
  (tolistmd U t)
    apply propositional_extensionality.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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset (tolistmd U t) (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list (fun '(w, (k, a)) => P (w, (k, a)))
  (tolistmd U t)
    induction (tolistmd U 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: Type
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset [] (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list (fun '(w, (k, a)) => P (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
A: Type
P: W * (K * A) -> Prop
t: U A
a: W * (K * A)
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w : W) (k : K) (a0 : A),
 ContainerFunctor.tosubset (a :: l) (w, (k, a0)) ->
 P (w, (k, a0))) <->
mapReduce_list 
  (fun '(w, (k, a)) => P (w, (k, a))) 
  (a :: l)
    -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
P: W * (K * A) -> Prop
t: U A
(forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset [] (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list (fun '(w, (k, a)) => P (w, (k, a))) [] cbv; intuition.
    -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
P: W * (K * A) -> Prop
t: U A
a: W * (K * A)
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w : W) (k : K) (a0 : A),
 ContainerFunctor.tosubset (a :: l) (w, (k, a0)) ->
 P (w, (k, a0))) <->
mapReduce_list (fun '(w, (k, a)) => P (w, (k, a)))
  (a :: l) destruct a as [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
A: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w0 : W) (k0 : K) (a0 : A),
 ContainerFunctor.tosubset ((w, (k, a)) :: l)
   (w0, (k0, a0)) -> P (w0, (k0, a0))) <->
mapReduce_list (fun '(w, (k, a)) => P (w, (k, a)))
  ((w, (k, a)) :: l) 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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w0 : W) (k0 : K) (a0 : A),
 (w, (k, a)) = (w0, (k0, a0)) \/
 List.In (w0, (k0, a0)) l -> P (w0, (k0, a0))) <->
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l)
      split.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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w0 : W) (k0 : K) (a0 : A),
 (w, (k, a)) = (w0, (k0, a0)) \/
 List.In (w0, (k0, a0)) l -> P (w0, (k0, a0))) ->
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l)
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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l) ->
forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
      +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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
(forall (w0 : W) (k0 : K) (a0 : A),
 (w, (k, a)) = (w0, (k0, a0)) \/
 List.In (w0, (k0, a0)) l -> P (w0, (k0, a0))) ->
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l) 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: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l) split.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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
P (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
A: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
crush_list (map (fun '(w, (k, a)) => P (w, (k, a))) l)
        *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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
P (w, (k, 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: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
(w, (k, a)) = (w, (k, a)) \/ List.In (w, (k, a)) l 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: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
crush_list (map (fun '(w, (k, a)) => P (w, (k, a))) l) apply IHl.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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
hyp: forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> 
P (w0, (k0, a0))
forall (w : W) (k : K) (a : A),
ContainerFunctor.tosubset l (w, (k, a)) ->
P (w, (k, 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
A: Type
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
P (w, (k, a))
● crush_list
    (map (fun '(w, (k, a)) => P (w, (k, a))) l) ->
forall (w0 : W) (k0 : K) (a0 : A),
(w, (k, a)) = (w0, (k0, a0)) \/
List.In (w0, (k0, a0)) l -> P (w0, (k0, a0)) introv [case1 case2] [Heq | 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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
case1: P (w, (k, a))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
w0: W
k0: K
a0: A
Heq: (w, (k, a)) = (w0, (k0, a0))
P (w0, (k0, a0))
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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
case1: P (w, (k, a))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
w0: W
k0: K
a0: A
Hin: List.In (w0, (k0, a0)) l
P (w0, (k0, a0))
        *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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
case1: P (w, (k, a))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
w0: W
k0: K
a0: A
Heq: (w, (k, a)) = (w0, (k0, a0))
P (w0, (k0, a0)) inversion Heq; subst.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
P: W * (K * A) -> Prop
t: U A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
w0: W
k0: K
a0: A
Heq: (w0, (k0, a0)) = (w0, (k0, a0))
case1: P (w0, (k0, a0))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
P (w0, (k0, a0)) cbv in *; tauto.
        *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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
mapReduce_list
  (fun '(w, (k, a)) => P (w, (k, a))) l
case1: P (w, (k, a))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
w0: W
k0: K
a0: A
Hin: List.In (w0, (k0, a0)) l
P (w0, (k0, a0)) unfold mapReduce_list, compose in IHl.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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
case1: P (w, (k, a))
case2: crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
w0: W
k0: K
a0: A
Hin: List.In (w0, (k0, a0)) l
P (w0, (k0, a0))
          rewrite <- IHl in case2.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
P: W * (K * A) -> Prop
t: U A
w: W
k: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (k : K) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, (k, a))) <->
crush_list
  (map (fun '(w, (k, a)) => P (w, (k, a))) l)
case1: P (w, (k, a))
case2: forall (w : W) (k : K) (a : A),
ContainerFunctor.tosubset l (w, (k, a)) ->
P (w, (k, a))
w0: W
k0: K
a0: A
Hin: List.In (w0, (k0, a0)) l
P (w0, (k0, a0)) auto.
  Qed.

  Definition Forallkd_spec : forall {A} {k: K} (P: W * A -> Prop) (t: U A),
      (forall w a, (w, (k, a)) ∈md t -> P (w, a)) =
        Forallkd k (fun '(w, a) => P (w, a)) 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) (k : K) (P : W * A -> Prop)
  (t : U A),
(forall (w : W) (a : A), (w, (k, a)) ∈md t -> P (w, a)) =
Forallkd k (fun '(w, a) => P (w, a)) 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) (k : K) (P : W * A -> Prop)
  (t : U A),
(forall (w : W) (a : A), (w, (k, a)) ∈md t -> P (w, a)) =
Forallkd k (fun '(w, a) => P (w, a)) 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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A), (w, (k, a)) ∈md t -> P (w, a)) =
Forallkd k (fun '(w, a) => P (w, a)) t
    unfold Forallkd, Forallmd, tosetmd.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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 (ContainerFunctor.tosubset ∘ tolistmd U) t
   (w, (k, a)) -> P (w, a)) =
mapReducekd U k (fun '(w, a) => P (w, a)) t
    rewrite (mapReducekd_to_mapReducemd 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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 (ContainerFunctor.tosubset ∘ tolistmd U) t
   (w, (k, a)) -> P (w, a)) =
mapReducemd U
  (tgt_def k (fun '(w, a) => P (w, a)) (const Ƶ)) t
    rewrite (mapReducemd_through_tolist 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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 (ContainerFunctor.tosubset ∘ tolistmd U) t
   (w, (k, a)) -> P (w, a)) =
(mapReduce_list
   (fun '(w, (k0, a)) =>
    tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
      k0 (w, a)) ∘ tolistmd U) 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
A: Type
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 ContainerFunctor.tosubset (tolistmd U t) (w, (k, a)) ->
 P (w, a)) =
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (w, a)) (tolistmd U t)
    apply propositional_extensionality.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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 ContainerFunctor.tosubset (tolistmd U t) (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (w, a)) (tolistmd U t)
    induction (tolistmd U 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: Type
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 ContainerFunctor.tosubset [] (w, (k, a)) -> P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (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
k: K
P: W * A -> Prop
t: U A
a: W * (K * A)
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
(forall (w : W) (a0 : A),
 ContainerFunctor.tosubset (a :: l) (w, (k, a0)) ->
 P (w, a0)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) 
  (a :: l)
    -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
k: K
P: W * A -> Prop
t: U A
(forall (w : W) (a : A),
 ContainerFunctor.tosubset [] (w, (k, a)) -> P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (w, a)) [] cbv; intuition.
    -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
k: K
P: W * A -> Prop
t: U A
a: W * (K * A)
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
(forall (w : W) (a0 : A),
 ContainerFunctor.tosubset (a :: l) (w, (k, a0)) ->
 P (w, a0)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (w, a)) (a :: l) destruct a as [w [j 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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
(forall (w0 : W) (a0 : A),
 ContainerFunctor.tosubset ((w, (j, a)) :: l)
   (w0, (k, a0)) -> P (w0, a0)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k (fun '(w0, a0) => P (w0, a0)) (const Ƶ)
     k0 (w, a)) ((w, (j, a)) :: l)
      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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) <->
tgt_def k (fun '(w, a) => P (w, a)) (const Ƶ) j (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        tgt_def k (fun '(w0, a0) => P (w0, a0))
          (const Ƶ) k0 (w, a)) l) unfold tgt_def.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) <->
(if k == j then fun '(w, a) => P (w, a) else const Ƶ)
  (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l)
      destruct_eq_args k 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
A: Type
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (j, a0)) \/
 List.In (w0, (j, a0)) l -> P (w0, a0)) <->
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l)
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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> 
 P (w0, a0)) <->
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (
          w, a)) l)
      {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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (j, a0)) \/
 List.In (w0, (j, a0)) l -> P (w0, a0)) <->
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) split.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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (j, a0)) \/
 List.In (w0, (j, a0)) l -> P (w0, a0)) ->
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l)
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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (
          w, a)) l) ->
forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/ List.In (w0, (j, a0)) l ->
P (w0, a0)
        +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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (j, a0)) \/
 List.In (w0, (j, a0)) l -> P (w0, a0)) ->
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) 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: Type
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) split.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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
P (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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
          *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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
P (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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
P (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: Type
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
(w, (j, a)) = (w, (j, a)) \/ List.In (w, (j, a)) l 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: Type
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (w, a)) l) apply IHl.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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/
List.In (w0, (j, a0)) l -> 
P (w0, a0)
forall (w : W) (a : A),
ContainerFunctor.tosubset l (w, (j, a)) -> P (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
A: Type
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
P (w, a)
● crush_list
    (map
       (fun '(w, (k, a)) =>
        (if j == k
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) ->
forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (j, a0)) \/ List.In (w0, (j, a0)) l ->
P (w0, a0) introv [case1 case2] [Heq | 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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
case1: P (w, a)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Heq: (w, (j, a)) = (w0, (j, a0))
P (w0, a0)
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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
case1: P (w, a)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (j, a0)) l
P (w0, a0)
          *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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
case1: P (w, a)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Heq: (w, (j, a)) = (w0, (j, a0))
P (w0, a0) inversion Heq; subst.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
P: W * A -> Prop
t: U A
j: K
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
w0: W
a0: A
Heq: (w0, (j, a0)) = (w0, (j, a0))
case1: P (w0, a0)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
P (w0, a0) cbv in *; tauto.
          *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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k, a)) =>
   tgt_def j 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k (
     w, a)) l
DESTR_EQs: j = j
case1: P (w, a)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (j, a0)) l
P (w0, a0) unfold mapReduce_list, compose in IHl.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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
crush_list
  (map
     (fun '(w, (k, a)) =>
      tgt_def j 
        (fun '(w0, a0) => P (w0, a0)) 
        (const Ƶ) k (
        w, a)) l)
DESTR_EQs: j = j
case1: P (w, a)
case2: crush_list
  (map
     (fun '(w, (k, a)) =>
      (if j == k
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (j, a0)) l
P (w0, a0)
            rewrite <- IHl in case2.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
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (j, a)) ->
 P (w, a)) <->
crush_list
  (map
     (fun '(w, (k, a)) =>
      tgt_def j 
        (fun '(w0, a0) => P (w0, a0)) 
        (const Ƶ) k (
        w, a)) l)
DESTR_EQs: j = j
case1: P (w, a)
case2: forall (w : W) (a : A),
ContainerFunctor.tosubset l (w, (j, a)) ->
P (w, a)
w0: W
a0: A
Hin: List.In (w0, (j, a0)) l
P (w0, a0) 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
A: Type
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) <->
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l)
      {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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) <->
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) split.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) ->
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l)
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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (
          w, a)) l) ->
forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/ List.In (w0, (k, a0)) l ->
P (w0, a0)
        +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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(forall (w0 : W) (a0 : A),
 (w, (j, a)) = (w0, (k, a0)) \/
 List.In (w0, (k, a0)) l -> P (w0, a0)) ->
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) 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: Type
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) split.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
const Ƶ (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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
          *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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
const Ƶ (w, a) cbv.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
True 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: Type
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (w, a)) l) apply IHl.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/
List.In (w0, (k, a0)) l -> 
P (w0, a0)
forall (w : W) (a : A),
ContainerFunctor.tosubset l (w, (k, a)) -> P (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
A: Type
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
const Ƶ (w, a)
● crush_list
    (map
       (fun '(w, (k0, a)) =>
        (if k == k0
         then fun '(w0, a0) => P (w0, a0)
         else const Ƶ) (w, a)) l) ->
forall (w0 : W) (a0 : A),
(w, (j, a)) = (w0, (k, a0)) \/ List.In (w0, (k, a0)) l ->
P (w0, a0) introv [case1 case2] [Heq | 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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Heq: (w, (j, a)) = (w0, (k, a0))
P (w0, a0)
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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (k, a0)) l
P (w0, a0)
          *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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Heq: (w, (j, a)) = (w0, (k, a0))
P (w0, a0) inversion Heq; subst.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
k: K
P: W * A -> Prop
t: U A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQs, DESTR_NEQ: k <> k
w0: W
a0: A
Heq: (w0, (k, a0)) = (w0, (k, a0))
case1: const Ƶ (w0, a0)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
P (w0, a0) cbv in *; tauto.
          *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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
mapReduce_list
  (fun '(w, (k0, a)) =>
   tgt_def k 
     (fun '(w0, a0) => P (w0, a0)) 
     (const Ƶ) k0 (
     w, a)) l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (k, a0)) l
P (w0, a0) unfold mapReduce_list, compose in IHl.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
crush_list
  (map
     (fun '(w, (k0, a)) =>
      tgt_def k 
        (fun '(w0, a0) => P (w0, a0)) 
        (const Ƶ) k0 (
        w, a)) l)
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: crush_list
  (map
     (fun '(w, (k0, a)) =>
      (if k == k0
       then fun '(w0, a0) => P (w0, a0)
       else const Ƶ) (
        w, a)) l)
w0: W
a0: A
Hin: List.In (w0, (k, a0)) l
P (w0, a0)
            rewrite <- IHl in case2.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
k: K
P: W * A -> Prop
t: U A
w: W
j: K
a: A
l: list (W * (K * A))
IHl: (forall (w : W) (a : A),
 ContainerFunctor.tosubset l (w, (k, a)) ->
 P (w, a)) <->
crush_list
  (map
     (fun '(w, (k0, a)) =>
      tgt_def k 
        (fun '(w0, a0) => P (w0, a0)) 
        (const Ƶ) k0 (
        w, a)) l)
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
case1: const Ƶ (w, a)
case2: forall (w : W) (a : A),
ContainerFunctor.tosubset l (w, (k, a)) ->
P (w, a)
w0: W
a0: A
Hin: List.In (w0, (k, a0)) l
P (w0, a0) auto. }
  Qed.

End forall_and_exists.