Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
From Tealeaves Require Import
  Classes.Categorical.ContainerFunctor
  Classes.Multisorted.DecoratedTraversableMonad
  Functors.List
  Functors.Subset
  Functors.Constant.

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

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

(** * Sorted lists with context *)
(**********************************************************************)
Section list.

  Context
    `{ix: Index}
    `{Monoid W}.

  Instance: MReturn (fun k A => list (W * (K * A))) :=
    fun A (k: K) (a: A) =>
      [(Ƶ, (k, a))].

  (** This operation is a context- and tag-sensitive substitution
   operation on lists of annotated values. It is used internally to
   reason about the interaction between <<mbinddt>> and
   <<tolistmd>>. *)
  Fixpoint mbinddt_list
           `(f: forall (k: K), W * A -> list (W * (K * B)))
           (l: list (W * (K * A))): list (W * (K * B)) :=
    match l with
    | nil => nil
    | cons (w, (k, a)) rest =>
      map (F := list) (incr w) (f k (w, a)) ++ mbinddt_list f rest
    end.

  
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))), mbinddt_list f [] = []
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))), mbinddt_list f [] = []
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

mbinddt_list f [] = []
easy. Qed.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (k : K) (a : A), mbinddt_list f (mret (fun (_ : K) (A0 : Type) => list (W * (K * A0))) k a) = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (k : K) (a : A), mbinddt_list f (mret (fun (_ : K) (A0 : Type) => list (W * (K * A0))) k a) = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

mbinddt_list f (mret (fun (_ : K) (A : Type) => list (W * (K * A))) k a) = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

map (incr Ƶ) (f k (Ƶ, a)) ++ [] = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

map (incr Ƶ) (f k (Ƶ, a)) = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

map id (f k (Ƶ, a)) = f k (Ƶ, a)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A
id = incr Ƶ
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

map id (f k (Ƶ, a)) = f k (Ƶ, a)
now rewrite (fun_map_id).
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A

id = incr Ƶ
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A
w: W
k2: K
b: B

id (w, (k2, b)) = incr Ƶ (w, (k2, b))
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
k: K
a: A
w: W
k2: K
b: B

id (w, (k2, b)) = (Ƶ ● w, (k2, b))
now simpl_monoid. Qed.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (w : W) (k : K) (a : A) (l : list (W * (K * A))), mbinddt_list f ((w, (k, a)) :: l) = map (incr w) (f k (w, a)) ++ mbinddt_list f l
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (w : W) (k : K) (a : A) (l : list (W * (K * A))), mbinddt_list f ((w, (k, a)) :: l) = map (incr w) (f k (w, a)) ++ mbinddt_list f l
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
w: W
k: K
a: A
l: list (W * (K * A))

mbinddt_list f ((w, (k, a)) :: l) = map (incr w) (f k (w, a)) ++ mbinddt_list f l
easy. Qed.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (l1 l2 : list (W * (K * A))), mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))) (l1 l2 : list (W * (K * A))), mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
l1, l2: list (W * (K * A))

mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
l2: list (W * (K * A))

mbinddt_list f ([] ++ l2) = mbinddt_list f [] ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
a: W * (K * A)
l1, l2: list (W * (K * A))
IHl1: mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2
mbinddt_list f ((a :: l1) ++ l2) = mbinddt_list f (a :: l1) ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
l2: list (W * (K * A))

mbinddt_list f ([] ++ l2) = mbinddt_list f [] ++ mbinddt_list f l2
easy.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
a: W * (K * A)
l1, l2: list (W * (K * A))
IHl1: mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2

mbinddt_list f ((a :: l1) ++ l2) = mbinddt_list f (a :: l1) ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
w: W
k: K
a: A
l1, l2: list (W * (K * A))
IHl1: mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2

mbinddt_list f (((w, (k, a)) :: l1) ++ l2) = mbinddt_list f ((w, (k, a)) :: l1) ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
w: W
k: K
a: A
l1, l2: list (W * (K * A))
IHl1: mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2

map (incr w) (f k (w, a)) ++ mbinddt_list f (l1 ++ l2) = (map (incr w) (f k (w, a)) ++ mbinddt_list f l1) ++ mbinddt_list f l2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
w: W
k: K
a: A
l1, l2: list (W * (K * A))
IHl1: mbinddt_list f (l1 ++ l2) = mbinddt_list f l1 ++ mbinddt_list f l2

map (incr w) (f k (w, a)) ++ mbinddt_list f l1 ++ mbinddt_list f l2 = (map (incr w) (f k (w, a)) ++ mbinddt_list f l1) ++ mbinddt_list f l2
now rewrite List.app_assoc. Qed.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))), ApplicativeMorphism (const (list (W * (K * A)))) (const (list (W * (K * B)))) (const (mbinddt_list f))
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W

forall (A B : Type) (f : K -> W * A -> list (W * (K * B))), ApplicativeMorphism (const (list (W * (K * A)))) (const (list (W * (K * B)))) (const (mbinddt_list f))
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

ApplicativeMorphism (const (list (W * (K * A)))) (const (list (W * (K * B)))) (const (mbinddt_list f))
eapply ApplicativeMorphism_monoid_morphism.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

Monoid_Morphism (list (W * (K * A))) (list (W * (K * B))) (mbinddt_list f)
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

mbinddt_list f Ƶ = Ƶ
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
forall a1 a2 : list (W * (K * A)), mbinddt_list f (a1 ● a2) = mbinddt_list f a1 ● mbinddt_list f a2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

mbinddt_list f Ƶ = Ƶ
easy.
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))

forall a1 a2 : list (W * (K * A)), mbinddt_list f (a1 ● a2) = mbinddt_list f a1 ● mbinddt_list f a2
ix: Index
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: K -> W * A -> list (W * (K * B))
a1, a2: list (W * (K * A))

mbinddt_list f (a1 ● a2) = mbinddt_list f a1 ● mbinddt_list f a2
apply mbinddt_list_app. Qed. End list. (** * Shape and Contents *) (**********************************************************************) (** ** Operations *) (**********************************************************************) Section shape_and_contents. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W T}. Definition shape {A}: U A -> U unit := mmap U (allK (const tt)). Definition tolistmd_gen_loc {A}: K -> W * A -> list (W * (K * A)) := fun k '(w, a) => [(w, (k, a))]. Definition tolistmd_gen {A} (fake: Type): U A -> list (W * (K * A)) := mmapdt (B := fake) U (const (list (W * (K * A)))) tolistmd_gen_loc. Definition tolistmd {A}: U A -> list (W * (K * A)) := tolistmd_gen False. Definition tosetmd {A}: U A -> W * (K * A) -> Prop := tosubset (F := list) ∘ tolistmd. Definition tolistm {A}: U A -> list (K * A) := map (F := list) extract ∘ tolistmd. Definition tosetm {A}: U A -> K * A -> Prop := tosubset (F := list) ∘ tolistm. Fixpoint filterk {A} (k: K) (l: list (W * (K * A))): list (W * A) := match l with | nil => nil | cons (w, (j, a)) ts => if k == j then (w, a) :: filterk k ts else filterk k ts end. Definition toklistd {A} (k: K): U A -> list (W * A) := filterk k ∘ tolistmd. Definition toksetd {A} (k: K): U A -> W * A -> Prop := tosubset (F := list) ∘ toklistd k. Definition toklist {A} (k: K): U A -> list A := map (F := list) extract ∘ @toklistd A k. End shape_and_contents. (** ** Notations *) (**********************************************************************) Module Notations. Notation "x ∈md t" := (tosetmd _ t x) (at level 50): tealeaves_multi_scope. Notation "x ∈m t" := (tosetm _ t x) (at level 50): tealeaves_multi_scope. End Notations. Import Notations. (** ** Rewriting Rules for <<filterk>> *) (**********************************************************************) Section rw_filterk. Context `{ix: Index} {W A: Type} (k: K). Implicit Types (l: list (W * (K * A))) (w: W) (a: A).
ix: Index
W, A: Type
k: K

filterk k ([] : list (W * (K * A))) = []
ix: Index
W, A: Type
k: K

filterk k ([] : list (W * (K * A))) = []
reflexivity. Qed.
ix: Index
W, A: Type
k: K

forall l w a, filterk k ((w, (k, a)) :: l) = (w, a) :: filterk k l
ix: Index
W, A: Type
k: K

forall l w a, filterk k ((w, (k, a)) :: l) = (w, a) :: filterk k l
ix: Index
W, A: Type
k: K
l: list (W * (K * A))
w: W
a: A

filterk k ((w, (k, a)) :: l) = (w, a) :: filterk k l
ix: Index
W, A: Type
k: K
l: list (W * (K * A))
w: W
a: A

(if k == k then (w, a) :: filterk k l else filterk k l) = (w, a) :: filterk k l
compare values k and k. Qed.
ix: Index
W, A: Type
k: K

forall l w a (j : K), j <> k -> filterk k ((w, (j, a)) :: l) = filterk k l
ix: Index
W, A: Type
k: K

forall l w a (j : K), j <> k -> filterk k ((w, (j, a)) :: l) = filterk k l
ix: Index
W, A: Type
k: K
l: list (W * (K * A))
w: W
a: A
j: K
H: j <> k

filterk k ((w, (j, a)) :: l) = filterk k l
ix: Index
W, A: Type
k: K
l: list (W * (K * A))
w: W
a: A
j: K
H: j <> k

(if k == j then (w, a) :: filterk k l else filterk k l) = filterk k l
compare values k and j. Qed.
ix: Index
W, A: Type
k: K

forall l1 l2, filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
ix: Index
W, A: Type
k: K

forall l1 l2, filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
ix: Index
W, A: Type
k: K
l1, l2: list (W * (K * A))

filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
ix: Index
W, A: Type
k: K
l2: list (W * (K * A))

filterk k ([] ++ l2) = filterk k [] ++ filterk k l2
ix: Index
W, A: Type
k: K
a: W * (K * A)
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
filterk k ((a :: l1) ++ l2) = filterk k (a :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
l2: list (W * (K * A))

filterk k ([] ++ l2) = filterk k [] ++ filterk k l2
reflexivity.
ix: Index
W, A: Type
k: K
a: W * (K * A)
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2

filterk k ((a :: l1) ++ l2) = filterk k (a :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
i: K
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2

filterk k (((w, (i, a)) :: l1) ++ l2) = filterk k ((w, (i, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

filterk k (((w, (k, a)) :: l1) ++ l2) = filterk k ((w, (k, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
i: K
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_NEQ: i <> k
DESTR_NEQs: k <> i
filterk k (((w, (i, a)) :: l1) ++ l2) = filterk k ((w, (i, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

filterk k (((w, (k, a)) :: l1) ++ l2) = filterk k ((w, (k, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

filterk k ((w, (k, a)) :: l1 ++ l2) = filterk k ((w, (k, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

(w, a) :: filterk k (l1 ++ l2) = filterk k ((w, (k, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

(w, a) :: filterk k (l1 ++ l2) = ((w, a) :: filterk k l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_EQs: k = k

(w, a) :: filterk k (l1 ++ l2) = (w, a) :: filterk k l1 ++ filterk k l2
now rewrite <- IHl1.
ix: Index
W, A: Type
k: K
w: W
i: K
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_NEQ: i <> k
DESTR_NEQs: k <> i

filterk k (((w, (i, a)) :: l1) ++ l2) = filterk k ((w, (i, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
i: K
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_NEQ: i <> k
DESTR_NEQs: k <> i

filterk k ((w, (i, a)) :: l1 ++ l2) = filterk k ((w, (i, a)) :: l1) ++ filterk k l2
ix: Index
W, A: Type
k: K
w: W
i: K
a: A
l1, l2: list (W * (K * A))
IHl1: filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
DESTR_NEQ: i <> k
DESTR_NEQs: k <> i

filterk k (l1 ++ l2) = filterk k ((w, (i, a)) :: l1) ++ filterk k l2
rewrite filterk_cons_neq; auto. Qed. End rw_filterk. #[export] Hint Rewrite @filterk_nil @filterk_cons_eq @filterk_cons_neq @filterk_app: tea_list. From Tealeaves Require Import Functors.List Functors.Constant. Import Product.Notations. Import Monoid.Notations. Import List.ListNotations. Open Scope list_scope. (** ** Auxiliary Lemmas for constant Applicative Functors*) (**********************************************************************) Section lemmas. #[local] Generalizable Variable M. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W 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
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B, A: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B, A: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B, A: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = map (mmap U (const exfalso)) ∘ mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
B, A: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = mbinddt U (const M) (fun k : K => map (mmap (T k) (const exfalso)) ∘ f k)
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake1, fake2, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A, B: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) (f : forall k : K, W * A -> const M (T k fake1)) = mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
fake1, fake2, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A, B: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) (f : forall k : K, W * A -> const M (T k fake1)) = mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
fake1, fake2, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A, B: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) (f : forall k : K, W * A -> const M (T k fake1)) = mbinddt U (const M) (f : forall k : K, W * A -> const M (T k 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
fake1, fake2, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A, B: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = mbinddt 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
fake1, fake2, M: Type
op: Monoid_op M
unit0: Monoid_unit M
H1: Monoid M
A, B: Type
f: forall k : K, W * A -> const M (T k B)

mbinddt U (const M) f = mbinddt U (const M) f
easy. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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 fake A : Type, tolistmd_gen U False = tolistmd_gen U fake
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall fake A : Type, tolistmd_gen U False = tolistmd_gen U fake
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A: Type

tolistmd_gen U False = tolistmd_gen U fake
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A: Type

tolistmd_gen U False = mbinddt U (const (list (W * (K * A)))) (mapMret ◻ tolistmd_gen_loc)
now rewrite (mbinddt_constant_applicative2 fake False). Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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 fake1 fake2 A : Type, tolistmd_gen U fake1 = tolistmd_gen U 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

forall fake1 fake2 A : Type, tolistmd_gen U fake1 = tolistmd_gen U 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
fake1, fake2, A: Type

tolistmd_gen U fake1 = tolistmd_gen U 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
fake1, fake2, A: Type

tolistmd_gen U False = tolistmd_gen U 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
fake1, fake2, A: Type

tolistmd_gen U False = tolistmd_gen U False
easy. Qed. End lemmas. (** ** Relating <<∈m>> and <<∈md>> *) (**********************************************************************) Section DTM_membership_lemmas. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W 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 (k : K) (A : Type) (a : A) (t : U A), (k, a) ∈m t <-> (exists w : W, (w, (k, a)) ∈md 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 (k : K) (A : Type) (a : A) (t : U A), (k, a) ∈m t <-> (exists w : W, (w, (k, a)) ∈md 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
k: K
A: Type
a: A
t: U A

(k, a) ∈m t <-> (exists w : W, (w, (k, a)) ∈md 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
k: K
A: Type
a: A
t: U A

tosubset (map extract (tolistmd U t)) (k, a) <-> (exists w : W, tosubset (tolistmd U t) (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
k: K
A: Type
a: A
t: U A

tosubset (map extract []) (k, a) <-> (exists w : W, tosubset [] (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
k: K
A: Type
a: A
t: U A
a0: W * (K * A)
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
tosubset (map extract (a0 :: l)) (k, a) <-> (exists w : W, tosubset (a0 :: l) (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
k: K
A: Type
a: A
t: U A

tosubset (map extract []) (k, a) <-> (exists w : W, tosubset [] (w, (k, a)))
cbv; split; intros []; 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
k: K
A: Type
a: A
t: U A
a0: W * (K * A)
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

tosubset (map extract (a0 :: l)) (k, a) <-> (exists w : W, tosubset (a0 :: l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

tosubset (map extract ((w', (k', a')) :: l)) (k, a) <-> (exists w : W, tosubset ((w', (k', a')) :: l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

tosubset (extract (w', (k', a')) :: map extract l) (k, a) <-> (exists w : W, tosubset ((w', (k', a')) :: l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

({{extract (w', (k', a'))}} ∪ tosubset (map extract l)) (k, a) <-> (exists w : W, tosubset ((w', (k', a')) :: l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

({{extract (w', (k', a'))}} ∪ tosubset (map extract l)) (k, a) <-> (exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

{{extract (w', (k', a'))}} (k, a) \/ tosubset (map extract l) (k, a) <-> (exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))

{{extract (w', (k', a'))}} (k, a) \/ (exists w : W, tosubset l (w, (k, a))) <-> (exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
Hfst: {{extract (w', (k', a'))}} (k, a)

exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
Hrest: tosubset l (w, (k, a))
exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest1: {{(w', (k', a'))}} (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/ (exists w : W, tosubset l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/ (exists w : W, tosubset l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
Hfst: {{extract (w', (k', a'))}} (k, a)

exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
Hfst: {{extract (w', (k', a'))}} (k, a)

({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
Hfst: {{extract (w', (k', a'))}} (k, a)

{{(w', (k', a'))}} (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
Hfst: {{extract (w', (k', a'))}} (k, a)

{{(w', (k, a))}} (w', (k, a))
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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
Hrest: tosubset l (w, (k, a))

exists w : W, ({{(w', (k', a'))}} ∪ tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
Hrest: tosubset l (w, (k, a))

({{(w', (k', a'))}} ∪ tosubset l) (w, (k, a))
now right.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest1: {{(w', (k', a'))}} (w, (k, a))

{{extract (w', (k', a'))}} (k, a) \/ (exists w : W, tosubset l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest1: {{(w', (k', a'))}} (w, (k, a))

{{extract (w', (k', a'))}} (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest1: (w', (k', a')) = (w, (k, a))

{{extract (w', (k', a'))}} (k, a)
now inversion rest1.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

{{extract (w', (k', a'))}} (k, a) \/ (exists w : W, tosubset l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

exists w : W, tosubset l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

tosubset (map extract l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

(tosubset ∘ map extract) l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

(map extract ∘ tosubset) l (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

map extract (tosubset l) (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
k: K
A: Type
a: A
t: U A
w': W
k': K
a': A
l: list (W * (K * A))
IHl: tosubset (map extract l) (k, a) <-> (exists w : W, tosubset l (w, (k, a)))
w: W
rest2: tosubset l (w, (k, a))

tosubset l (w, (k, a)) /\ extract (w, (k, a)) = (k, a)
easy. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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 (k : K) (A : Type) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t -> (k, a) ∈m 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 (k : K) (A : Type) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t -> (k, a) ∈m 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
k: K
A: Type
a: A
w: W
t: U A
H1: (w, (k, a)) ∈md t

(k, a) ∈m 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
k: K
A: Type
a: A
w: W
t: U A
H1: (w, (k, a)) ∈md t

exists w : W, (w, (k, a)) ∈md t
eauto. Qed. End DTM_membership_lemmas. (** ** Characterizing Membership in List Operations *) (**********************************************************************) Section DTM_tolist. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W 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) (l : list (W * (K * A))) (k : K) (a : A) (w : W), (w, a) ∈ filterk k l <-> (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

forall (A : Type) (l : list (W * (K * A))) (k : K) (a : A) (w : W), (w, a) ∈ filterk k l <-> (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
l: list (W * (K * A))
k: K
a: A
w: W

(w, a) ∈ filterk k l <-> (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
k: K
a: A
w: W

(w, a) ∈ filterk k [] <-> (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
a0: W * (K * A)
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
(w, a) ∈ filterk k (a0 :: l) <-> (w, (k, a)) ∈ (a0 :: 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
a: A
w: W

(w, a) ∈ filterk k [] <-> (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
k: K
a: A
w: W

False <-> False
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
a0: W * (K * A)
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l

(w, a) ∈ filterk k (a0 :: l) <-> (w, (k, a)) ∈ (a0 :: 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l

(w, a) ∈ filterk k ((w', (j, a')) :: l) <-> (w, (k, a)) ∈ ((w', (j, 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l

List.In (w, a) (if k == j then (w', a') :: filterk k l else filterk k l) <-> (w', (j, a')) = (w, (k, a)) \/ List.In (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
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
IHl: (w, a) ∈ filterk j l <-> (w, (j, a)) ∈ l
DESTR_EQs: j = j

List.In (w, a) ((w', a') :: filterk j l) <-> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
List.In (w, a) (filterk k l) <-> (w', (j, a')) = (w, (k, a)) \/ List.In (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
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
IHl: (w, a) ∈ filterk j l <-> (w, (j, a)) ∈ l
DESTR_EQs: j = j

List.In (w, a) ((w', a') :: filterk j l) <-> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, 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
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
IHl: (w, a) ∈ filterk j l <-> (w, (j, a)) ∈ l
DESTR_EQs: j = j

(w', a') = (w, a) \/ List.In (w, a) (filterk j l) <-> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, 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
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
IHl: (w, a) ∈ filterk j l <-> (w, (j, a)) ∈ l
DESTR_EQs: j = j

(w', a') = (w, a) \/ (w, (j, a)) ∈ l <-> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W

(w', a') = (w, a) \/ (w, (j, a)) ∈ l <-> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W

(w', a') = (w, a) \/ (w, (j, a)) ∈ l -> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l -> (w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W

(w', a') = (w, a) \/ (w, (j, a)) ∈ l -> (w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp1: (w', a') = (w, a)

(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp2: (w, (j, a)) ∈ l
(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp1: (w', a') = (w, a)

(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
ix: Index
W, A: Type
j: K
l: list (W * (K * A))
a: A
w: W

(w, (j, a)) = (w, (j, a)) \/ List.In (w, (j, a)) l
now left.
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp2: (w, (j, a)) ∈ l

(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l
now right.
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W

(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l -> (w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W

(w', (j, a')) = (w, (j, a)) \/ List.In (w, (j, a)) l -> (w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp1: (w', (j, a')) = (w, (j, a))

(w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp2: List.In (w, (j, a)) l
(w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp1: (w', (j, a')) = (w, (j, a))

(w', a') = (w, a) \/ (w, (j, a)) ∈ l
ix: Index
W, A: Type
j: K
l: list (W * (K * A))
a: A
w: W

(w, a) = (w, a) \/ (w, (j, a)) ∈ l
now left.
ix: Index
W, A: Type
w': W
j: K
a': A
l: list (W * (K * A))
a: A
w: W
hyp2: List.In (w, (j, a)) l

(w', a') = (w, a) \/ (w, (j, a)) ∈ l
now right. }
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

List.In (w, a) (filterk k l) <-> (w', (j, a')) = (w, (k, a)) \/ List.In (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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

List.In (w, a) (filterk k l) <-> (w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

List.In (w, a) (filterk k l) -> (w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
(w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k l -> List.In (w, a) (filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

List.In (w, a) (filterk k l) -> (w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp: List.In (w, a) (filterk k l)

(w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k l
now right.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

(w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k l -> List.In (w, a) (filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k

(w', (j, a')) = (w, (k, a)) \/ (w, a) ∈ filterk k l -> List.In (w, a) (filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp1: (w', (j, a')) = (w, (k, a))

List.In (w, a) (filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp2: (w, a) ∈ filterk k l
List.In (w, a) (filterk k 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp1: (w', (j, a')) = (w, (k, a))

List.In (w, a) (filterk k 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
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQs, DESTR_NEQ: k <> k

List.In (w, a) (filterk k l)
contradiction.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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
w': W
j: K
a': A
l: list (W * (K * A))
k: K
a: A
w: W
IHl: (w, a) ∈ filterk k l <-> (w, (k, a)) ∈ l
DESTR_NEQ: k <> j
DESTR_NEQs: j <> k
hyp2: (w, a) ∈ filterk k l

List.In (w, a) (filterk k l)
auto. } Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t <-> (w, (k, a)) ∈ 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

forall (A : Type) (k : K) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t <-> (w, (k, a)) ∈ tolistmd U t
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (t : U A), (k, a) ∈m t <-> (k, a) ∈ tolistm 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

forall (A : Type) (k : K) (a : A) (t : U A), (k, a) ∈m t <-> (k, a) ∈ tolistm U t
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t <-> (w, a) ∈ toklistd U k 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) (a : A) (w : W) (t : U A), (w, (k, a)) ∈md t <-> (w, a) ∈ toklistd U k 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
a: A
w: W
t: U A

(w, (k, a)) ∈md t <-> (w, a) ∈ toklistd U k 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
a: A
w: W
t: U A

(w, (k, a)) ∈md t <-> (w, a) ∈ (filterk k ∘ 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
a: A
w: W
t: U A

(w, (k, a)) ∈md t <-> (w, a) ∈ filterk k (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
a: A
w: W
t: U A

(w, (k, a)) ∈md t <-> (w, (k, a)) ∈ tolistmd U t
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (t : U A), (k, a) ∈m t <-> a ∈ toklist U k 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) (a : A) (t : U A), (k, a) ∈m t <-> a ∈ toklist U k 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
a: A
t: U A

(k, a) ∈m t <-> a ∈ toklist U k 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
a: A
t: U A

(k, a) ∈m t <-> a ∈ (map extract ∘ toklistd U k) 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
a: A
t: U A

(k, a) ∈m t <-> a ∈ map extract (toklistd U k 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
a: A
t: U A

(k, a) ∈m t <-> (exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A

(k, a) ∈m t -> exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A
(exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = a) -> (k, a) ∈m 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
a: A
t: U A

(k, a) ∈m t -> exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A
hyp: (k, a) ∈m t

exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A
hyp: exists w : W, (w, (k, a)) ∈md t

exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A
w': W
hyp: (w', (k, a)) ∈md t

exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = 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
a: A
t: U A
w': W
hyp: (w', (k, a)) ∈md t

(w', a) ∈ toklistd U k t /\ extract (w', a) = 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
a: A
t: U A
w': W
hyp: (w', a) ∈ toklistd U k t

(w', a) ∈ toklistd U k t /\ extract (w', a) = 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
a: A
t: U A

(exists a0 : W * A, a0 ∈ toklistd U k t /\ extract a0 = a) -> (k, a) ∈m 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
a: A
t: U A
w': W
a': A
hyp1: (w', a') ∈ toklistd U k t
hyp2: extract (w', a') = a

(k, a) ∈m 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
a: A
t: U A
w': W
a': A
hyp1: (w', a') ∈ toklistd U k t
hyp2: extract (w', a') = a

exists w : W, (w, (k, a)) ∈md 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
a: A
t: U A
w': W
a': A
hyp1: (w', a') ∈ toklistd U k t
hyp2: extract (w', a') = a

(w', (k, a)) ∈md 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
a: A
t: U A
w': W
a': A
hyp1: (w', (k, a')) ∈md t
hyp2: extract (w', a') = a

(w', (k, a)) ∈md 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
a: A
t: U A
w': W
a': A
hyp1: (w', (k, a')) ∈md t
hyp2: a' = a

(w', (k, a)) ∈md t
now subst. Qed. End DTM_tolist. (** ** Interaction between <<tolistmd>> and <<mret>>/<<mbindd>> *) (**********************************************************************) Section DTM_tolist. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W T}.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (a : A) (k : K), tolistmd_gen (T k) B (mret T k a) = [(Ƶ, (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

forall (A B : Type) (a : A) (k : K), tolistmd_gen (T k) B (mret T k a) = [(Ƶ, (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, B: Type
a: A
k: K

tolistmd_gen (T k) B (mret T k a) = [(Ƶ, (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, B: Type
a: A
k: K

mmapdt (T k) (const (list (W * (K * A)))) tolistmd_gen_loc (mret T k a) = [(Ƶ, (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, B: Type
a: A
k: K

(mmapdt (T k) (const (list (W * (K * A)))) tolistmd_gen_loc ∘ mret T k) a = [(Ƶ, (k, a))]
now rewrite mmapdt_comp_mret. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (k : K), tolistmd (T k) (mret T k a) = [(Ƶ, (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

forall (A : Type) (a : A) (k : K), tolistmd (T k) (mret T k a) = [(Ƶ, (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
a: A
k: K

tolistmd (T k) (mret T k a) = [(Ƶ, (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
a: A
k: K

tolistmd_gen (T k) False (mret T k a) = [(Ƶ, (k, a))]
apply tolistmd_gen_mret. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (k : K), tosetmd (T k) (mret T k a) = {{(Ƶ, (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

forall (A : Type) (a : A) (k : K), tosetmd (T k) (mret T k a) = {{(Ƶ, (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
a: A
k: K

tosetmd (T k) (mret T k a) = {{(Ƶ, (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
a: A
k: K

tosubset (tolistmd (T k) (mret T k a)) = {{(Ƶ, (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
a: A
k: K

tosubset [(Ƶ, (k, a))] = {{(Ƶ, (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
a: A
k: K

{{(Ƶ, (k, a))}} = {{(Ƶ, (k, a))}}
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (k : K), tolistm (T k) (mret T k a) = [(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

forall (A : Type) (a : A) (k : K), tolistm (T k) (mret T k a) = [(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
a: A
k: K

tolistm (T k) (mret T k a) = [(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
a: A
k: K

map extract (tolistmd (T k) (mret T k a)) = [(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
a: A
k: K

map extract [(Ƶ, (k, a))] = [(k, a)]
easy. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a : A) (k : K), tosetm (T k) (mret T k a) = {{(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

forall (A : Type) (a : A) (k : K), tosetm (T k) (mret T k a) = {{(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
a: A
k: K

tosetm (T k) (mret T k a) = {{(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
a: A
k: K

tosubset (tolistm (T k) (mret T k a)) = {{(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
a: A
k: K

tosubset [(k, a)] = {{(k, a)}}
apply tosubset_list_ret. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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 (fake A B : Type) (f : W * A ~k~> T B) (t : U A), tolistmd_gen U fake (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd_gen (T k) fake (f k (w, a))) (tolistmd_gen U fake t)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (fake A B : Type) (f : W * A ~k~> T B) (t : U A), tolistmd_gen U fake (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd_gen (T k) fake (f k (w, a))) (tolistmd_gen U fake t)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A

tolistmd_gen U fake (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd_gen (T k) fake (f k (w, a))) (tolistmd_gen U fake t)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) (mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

(mbinddt U (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) ∘ mbindd U f) t = mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) (mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) (mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = (mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) ∘ mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = (const (mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a)))) (U fake) ∘ mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = (const (mbinddt_list (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a)))) (U fake) ∘ mbinddt U (const (list (W * (K * A)))) (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = mbinddt U (const (list (W * (K * B)))) ((fun k : K => const (mbinddt_list (fun (k0 : K) '(w, a) => mbinddt (T k0) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k0 (w, a)))) (T k fake)) ◻ (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

mbinddt U (const (list (W * (K * B)))) (fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) t = mbinddt U (const (list (W * (K * B)))) ((fun k : K => const (mbinddt_list (fun (k0 : K) '(w, a) => mbinddt (T k0) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k0 (w, a)))) (T k fake)) ◻ (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A

(fun (k : K) '(w, a) => mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a))) = (fun k : K => const (mbinddt_list (fun (k0 : K) '(w, a) => mbinddt (T k0) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k0 (w, a)))) (T k fake)) ◻ (mapMret ◻ 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
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = ((fun k : K => const (mbinddt_list (fun (k0 : K) '(w, a) => mbinddt (T k0) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k0 (w, a)))) (T k fake)) ◻ (mapMret ◻ tolistmd_gen_loc)) k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = map (incr w) (mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) ++ []
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = const (map (incr w)) (U B) (mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a))) ++ []
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = const (map (incr w)) (U B) (mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc) (f k (w, a)))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = (const (map (incr w)) (U B) ∘ mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc)) (f k (w, a))
(* for some reason I can't rewrite without posing first. *)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A
rw:= dtp_mbinddt_morphism W T (T k) (const (list (W * (K * B)))) (const (list (W * (K * B)))): forall f : forall k : K, W * B -> const (list (W * (K * B))) (T k fake), const (map (incr w)) (T k fake) ∘ mbinddt (T k) (const (list (W * (K * B)))) f = mbinddt (T k) (const (list (W * (K * B)))) ((fun k : K => const (map (incr w)) (T k fake)) ◻ f)

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = (const (map (incr w)) (U B) ∘ mbinddt (T k) (const (list (W * (K * B)))) (mapMret ◻ tolistmd_gen_loc)) (f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A
rw:= dtp_mbinddt_morphism W T (T k) (const (list (W * (K * B)))) (const (list (W * (K * B)))): forall f : forall k : K, W * B -> const (list (W * (K * B))) (T k fake), const (map (incr w)) (T k fake) ∘ mbinddt (T k) (const (list (W * (K * B)))) f = mbinddt (T k) (const (list (W * (K * B)))) ((fun k : K => const (map (incr w)) (T k fake)) ◻ f)

mbinddt (T k) (const (list (W * (K * B)))) ((mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w)) (f k (w, a)) = mbinddt (T k) (const (list (W * (K * B)))) ((fun k : K => const (map (incr w)) (T k fake)) ◻ (mapMret ◻ tolistmd_gen_loc)) (f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
fake, A, B: Type
f: W * A ~k~> T B
t: U A
k: K
w: W
a: A
rw:= dtp_mbinddt_morphism W T (T k) (const (list (W * (K * B)))) (const (list (W * (K * B)))): forall f : forall k : K, W * B -> const (list (W * (K * B))) (T k fake), const (map (incr w)) (T k fake) ∘ mbinddt (T k) (const (list (W * (K * B)))) f = mbinddt (T k) (const (list (W * (K * B)))) ((fun k : K => const (map (incr w)) (T k fake)) ◻ f)

(mapMret ◻ tolistmd_gen_loc) ◻ allK (incr w) = (fun k : K => const (map (incr w)) (T k fake)) ◻ (mapMret ◻ tolistmd_gen_loc)
now ext k2 [w2 b]. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A), tolistmd U (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (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

forall (A B : Type) (f : W * A ~k~> T B) (t : U A), tolistmd U (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (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, B: Type
f: W * A ~k~> T B
t: U A

tolistmd U (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (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, B: Type
f: W * A ~k~> T B
t: U A

tolistmd_gen U False (mbindd U f t) = mbinddt_list (fun (k : K) '(w, a) => tolistmd_gen (T k) False (f k (w, a))) (tolistmd_gen U False t)
apply tolistmd_gen_mbindd. Qed. End DTM_tolist. (** ** Characterizing Occurrences Post-Operation *) (**********************************************************************) Section DTM_membership. Context (U: Type -> Type) `{MultiDecoratedTraversablePreModule W T U} `{! MultiDecoratedTraversableMonad W T}. (** *** Occurrences in <<mret>> *) (********************************************************************)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k1 k2 : K) (w : W), (w, (k2, a2)) ∈md mret T k1 a1 <-> w = Ƶ /\ k1 = k2 /\ a1 = 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

forall (A : Type) (a1 a2 : A) (k1 k2 : K) (w : W), (w, (k2, a2)) ∈md mret T k1 a1 <-> w = Ƶ /\ k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K
w: W

(w, (k2, a2)) ∈md mret T k1 a1 <-> w = Ƶ /\ k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K
w: W

{{(Ƶ, (k1, a1))}} (w, (k2, a2)) <-> w = Ƶ /\ k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K
w: W

(Ƶ, (k1, a1)) = (w, (k2, a2)) <-> w = Ƶ /\ k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K
w: W

(Ƶ, (k1, a1)) = (w, (k2, a2)) -> w = Ƶ /\ k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K
w: W
w = Ƶ /\ k1 = k2 /\ a1 = a2 -> (Ƶ, (k1, a1)) = (w, (k2, 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
a1, a2: A
k1, k2: K
w: W

(Ƶ, (k1, a1)) = (w, (k2, a2)) -> w = Ƶ /\ k1 = k2 /\ a1 = a2
inversion 1; now 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
a1, a2: A
k1, k2: K
w: W

w = Ƶ /\ k1 = k2 /\ a1 = a2 -> (Ƶ, (k1, a1)) = (w, (k2, 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
a1, a2: A
k1, k2: K
w: W
H1: w = Ƶ
H2: k1 = k2
H3: a1 = a2

(Ƶ, (k1, a1)) = (w, (k2, a2))
now subst. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k1 k2 : K), (k2, a2) ∈m mret T k1 a1 <-> k1 = k2 /\ a1 = 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

forall (A : Type) (a1 a2 : A) (k1 k2 : K), (k2, a2) ∈m mret T k1 a1 <-> k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K

(k2, a2) ∈m mret T k1 a1 <-> k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K

(exists w : W, (w, (k2, a2)) ∈md mret T k1 a1) <-> k1 = k2 /\ a1 = 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
a1, a2: A
k1, k2: K

(exists w : W, w = Ƶ /\ k1 = k2 /\ a1 = a2) <-> k1 = k2 /\ a1 = a2
firstorder. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k : K) (w : W), (w, (k, a2)) ∈md mret T k a1 <-> w = Ƶ /\ a1 = 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

forall (A : Type) (a1 a2 : A) (k : K) (w : W), (w, (k, a2)) ∈md mret T k a1 <-> w = Ƶ /\ a1 = 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
a1, a2: A
k: K
w: W

(w, (k, a2)) ∈md mret T k a1 <-> w = Ƶ /\ a1 = 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
a1, a2: A
k: K
w: W

w = Ƶ /\ k = k /\ a1 = a2 <-> w = Ƶ /\ a1 = a2
ix: Index
W: Type
mn_unit: Monoid_unit W
A: Type
a1, a2: A
k: K
w: W

w = Ƶ /\ k = k /\ a1 = a2 <-> w = Ƶ /\ a1 = a2
firstorder. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k j : K) (w : W), k <> j -> (w, (j, a2)) ∈md mret T k a1 <-> 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

forall (A : Type) (a1 a2 : A) (k j : K) (w : W), k <> j -> (w, (j, a2)) ∈md mret T k a1 <-> 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: Type
a1, a2: A
k, j: K
w: W
H1: k <> j

(w, (j, a2)) ∈md mret T k a1 <-> 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: Type
a1, a2: A
k, j: K
w: W
H1: k <> j

w = Ƶ /\ k = j /\ a1 = a2 <-> False
firstorder. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k : K), (k, a2) ∈m mret T k a1 <-> a1 = 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

forall (A : Type) (a1 a2 : A) (k : K), (k, a2) ∈m mret T k a1 <-> a1 = 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
a1, a2: A
k: K

(k, a2) ∈m mret T k a1 <-> a1 = 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
a1, a2: A
k: K

k = k /\ a1 = a2 <-> a1 = a2
firstorder. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, 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) (a1 a2 : A) (k j : K), k <> j -> (j, a2) ∈m mret T k a1 <-> 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

forall (A : Type) (a1 a2 : A) (k j : K), k <> j -> (j, a2) ∈m mret T k a1 <-> 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: Type
a1, a2: A
k, j: K
H1: k <> j

(j, a2) ∈m mret T k a1 <-> 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: Type
a1, a2: A
k, j: K
H1: k <> j

(exists w : W, (w, (j, a2)) ∈md mret T k a1) <-> 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: Type
a1, a2: A
k, j: K
H1: k <> j

(exists w : W, w = Ƶ /\ k = j /\ a1 = a2) <-> False
firstorder. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (l : list A) (f : A -> B), tosubset (map f l) = map f (tosubset 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

forall (A B : Type) (l : list A) (f : A -> B), tosubset (map f l) = map f (tosubset 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, B: Type
l: list A
f: A -> B

tosubset (map f l) = map f (tosubset 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, B: Type
l: list A
f: A -> B

(tosubset ∘ map f) l = (map f ∘ tosubset) 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, B: Type
l: list A
f: A -> B

(map f ∘ tosubset) l = (map f ∘ tosubset) l
reflexivity. Qed. (** *** Occurrences in <<mbindd>> with context *) (********************************************************************)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbindd U f t -> exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbindd U f t -> exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
hyp: (wtotal, (k2, b)) ∈md mbindd U f t

exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
hyp: tosubset (tolistmd U (mbindd U f t)) (wtotal, (k2, b))

exists (k1 : K) (w1 w2 : W) (a : A), tosubset (tolistmd U t) (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (tolistmd U t)) ( wtotal, (k2, b))

exists (k1 : K) (w1 w2 : W) (a : A), tosubset (tolistmd U t) (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) []) (wtotal, (k2, b))

exists (k1 : K) (w1 w2 : W) (a : A), tosubset [] (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
a: W * (K * A)
l: list (W * (K * A))
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (a :: l)) ( wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset (a :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) ( w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) []) (wtotal, (k2, b))

exists (k1 : K) (w1 w2 : W) (a : A), tosubset [] (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
inversion hyp.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
a: W * (K * A)
l: list (W * (K * A))
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (a :: l)) ( wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset (a :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) ((w, (k, a)) :: l)) ( wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp: tosubset (map (incr w) (tolistmd (T k) (f k (w, a))) ++ mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp: (tosubset (map (incr w) (tolistmd (T k) (f k (w, a)))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp1: tosubset (map (incr w) (tolistmd (T k) (f k (w, a)))) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp2: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) ( w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp1: tosubset (map (incr w) (tolistmd (T k) (f k (w, a)))) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp1: map (incr w) (tosubset (tolistmd (T k) (f k (w, a)))) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
k2': K
b': B
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2', b'))
hyp2: incr w (w2, (k2', b')) = (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

exists (k1 : K) (w1 w3 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

tosubset ((w, (k, a)) :: l) (w, (k, a)) /\ tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b)) /\ w ● w2 = w ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

tosubset ((w, (k, a)) :: l) (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, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))
tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))
w ● w2 = w ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

tosubset ((w, (k, a)) :: l) (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, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

({{(w, (k, a))}} ∪ tosubset l) (w, (k, a))
now left.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))
w ● w2 = w ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
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, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

w ● w2 = w ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
w2: W
hyp1: tosubset (tolistmd (T k) (f k (w, a))) (w2, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w ● w2, (k2, b)) -> exists (k1 : K) (w1 w3 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w3, (k2, b)) /\ w ● w2 = w1 ● w3
hyp2: incr w (w2, (k2, b)) = (w ● w2, (k2, b))

w ● w2 = w ● w2
easy. }
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp2: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b))
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp2: exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2
IHl: tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (wtotal, (k2, b)) -> exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
hyp2: exists (k1 : K) (w1 w2 : W) (a : A), tosubset l (w1, (k1, a)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))
hyp3: wtotal = w1 ● w2

exists (k1 : K) (w1 w2 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w1, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w1, a0))) (w2, (k2, b)) /\ wtotal = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

exists (k1 : K) (w3 w4 : W) (a0 : A), tosubset ((w, (k, a)) :: l) (w3, (k1, a0)) /\ tosubset (tolistmd (T k1) (f k1 (w3, a0))) (w4, (k2, b)) /\ w1 ● w2 = w3 ● w4
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

tosubset ((w, (k, a)) :: l) (w1, (?k1, ?a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))
tosubset (tolistmd (T ?k1) (f ?k1 (w1, ?a))) (w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

tosubset ((w, (k, a)) :: l) (w1, (?k1, ?a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

({{(w, (k, a))}} ∪ tosubset l) (w1, (?k1, ?a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

tosubset l (w1, (?k1, ?a))
eauto.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
w: W
k: K
a: A
l: list (W * (K * A))
k1: K
w1, w2: W
a': A
hyp1: tosubset l (w1, (k1, a'))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))

tosubset (tolistmd (T k1) (f k1 (w1, a'))) (w2, (k2, b))
auto. } Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2) -> (wtotal, (k2, b)) ∈md mbindd U f t
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2) -> (wtotal, (k2, b)) ∈md mbindd U f t
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
wtotal: W
b: B
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (w2, (k2, b)) ∈md f k1 (w1, a)
hyp3: wtotal = w1 ● w2

(wtotal, (k2, b)) ∈md mbindd U f t
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (w2, (k2, b)) ∈md f k1 (w1, a)

(w1 ● w2, (k2, b)) ∈md mbindd U f t
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
hyp1: tosubset (tolistmd U t) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))

tosubset (tolistmd U (mbindd U f t)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
hyp1: tosubset (tolistmd U t) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (tolistmd U t)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
hyp1: tosubset [] (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) []) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
a0: W * (K * A)
l: list (W * (K * A))
hyp1: tosubset (a0 :: l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))
tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (a0 :: l)) ( w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
hyp1: tosubset [] (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) []) (w1 ● w2, (k2, b))
inversion hyp1.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
a0: W * (K * A)
l: list (W * (K * A))
hyp1: tosubset (a0 :: l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) (a0 :: l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset ((w, (k', a')) :: l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) ((w, (k', a')) :: l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset ((w, (k', a')) :: l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (map (incr w) (tolistmd (T k') (f k' (w, a'))) ++ mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset ((w, (k', a')) :: l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: ({{(w, (k', a'))}} ∪ tosubset l) (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: {{(w, (k', a'))}} (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset l (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))
(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: {{(w, (k', a'))}} (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
l: list (W * (K * A))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w1) (tolistmd (T k1) (f k1 (w1, a)))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
l: list (W * (K * A))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (map (incr w1) (tolistmd (T k1) (f k1 (w1, a)))) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
l: list (W * (K * A))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

map (incr w1) (tosubset (tolistmd (T k1) (f k1 (w1, a)))) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
l: list (W * (K * A))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b)) /\ incr w1 (w2, (k2, b)) = (w1 ● w2, (k2, b))
now splits.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset l (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

(tosubset (map (incr w) (tolistmd (T k') (f k' (w, a')))) ∪ tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l)) (w1 ● w2, (k2, b))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1, w2: W
a: A
w: W
k': K
a': A
l: list (W * (K * A))
hyp1: tosubset l (w1, (k1, a))
hyp2: tosubset (tolistmd (T k1) (f k1 (w1, a))) (w2, (k2, b))
IHl: tosubset l (w1, (k1, a)) -> tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))

tosubset (mbinddt_list (fun (k : K) '(w, a) => tolistmd (T k) (f k (w, a))) l) (w1 ● w2, (k2, b))
now apply IHl in hyp1. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbindd U f t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbindd U f t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ wtotal = w1 ● w2)
split; auto using inmd_mbindd_iff1, inmd_mbindd_iff2. Qed. (** *** Corollaries for other operations *) (********************************************************************)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbind U f t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 a /\ wtotal = w1 ● w2)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : A ~k~> T B) (t : U A) (k2 : K) (wtotal : W) (b : B), (wtotal, (k2, b)) ∈md mbind U f t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 a /\ wtotal = w1 ● w2)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
wtotal: W
b: B

(wtotal, (k2, b)) ∈md mbind U f t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 a /\ wtotal = w1 ● w2)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
wtotal: W
b: B

(wtotal, (k2, b)) ∈md mbindd U (f ◻ allK extract) t <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 a /\ wtotal = w1 ● w2)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
wtotal: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ wtotal = w1 ● w2) <-> (exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 a /\ wtotal = w1 ● w2)
reflexivity. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : K -> W * A -> B) (t : U A) (k : K) (w : W) (b : B), (w, (k, b)) ∈md mmapd U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f 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

forall (A B : Type) (f : K -> W * A -> B) (t : U A) (k : K) (w : W) (b : B), (w, (k, b)) ∈md mmapd U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(w, (k, b)) ∈md mmapd U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(w, (k, b)) ∈md mbindd U (mret T ◻ f) t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k, b)) ∈md (mret T ◻ f) k1 (w1, a) /\ w = w1 ● w2) <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k, b)) ∈md (mret T ◻ f) k1 (w1, a) /\ w = w1 ● w2) <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2) <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2) -> exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B
(exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a)) -> exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2) -> exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: w2 = Ƶ
hyp2': k1 = k
hyp2'': f k1 (w1, a) = b
hyp3: w = w1 ● w2

exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w1: W
a: A
hyp1: (w1, (k, a)) ∈md t

exists a0 : A, (w1 ● Ƶ, (k, a0)) ∈md t /\ f k (w1, a) = f k (w1 ● Ƶ, 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, B: Type
f: K -> W * A -> B
t: U A
k: K
w1: W
a: A
hyp1: (w1, (k, a)) ∈md t

(w1 ● Ƶ, (k, a)) ∈md t /\ f k (w1, a) = f k (w1 ● Ƶ, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w1: W
a: A
hyp1: (w1, (k, a)) ∈md t

(w1, (k, a)) ∈md t /\ f k (w1, a) = f k (w1, 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, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B

(exists a : A, (w, (k, a)) ∈md t /\ b = f k (w, a)) -> exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
b: B
a: A
hyp1: (w, (k, a)) ∈md t
hyp2: b = f k (w, a)

exists (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
a: A
hyp1: (w, (k, a)) ∈md t

exists (k1 : K) (w1 w2 : W) (a0 : A), (w1, (k1, a0)) ∈md t /\ (w2 = Ƶ /\ k1 = k /\ f k1 (w1, a0) = f k (w, a)) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
a: A
hyp1: (w, (k, a)) ∈md t

(w, (k, a)) ∈md t
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
a: A
hyp1: (w, (k, a)) ∈md t
w = 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
A, B: Type
f: K -> W * A -> B
t: U A
k: K
w: W
a: A
hyp1: (w, (k, a)) ∈md t

w = w ● Ƶ
now simpl_monoid. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : K -> A -> B) (t : U A) (k : K) (w : W) (b : B), (w, (k, b)) ∈md mmap U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f 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

forall (A B : Type) (f : K -> A -> B) (t : U A) (k : K) (w : W) (b : B), (w, (k, b)) ∈md mmap U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
w: W
b: B

(w, (k, b)) ∈md mmap U f t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
w: W
b: B

(w, (k, b)) ∈md mmapd U (f ◻ allK extract) t <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
w: W
b: B

(exists a : A, (w, (k, a)) ∈md t /\ b = (f ◻ allK extract) k (w, a)) <-> (exists a : A, (w, (k, a)) ∈md t /\ b = f k a)
easy. Qed. (** *** Occurrences without context *) (********************************************************************)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (b : B), (k2, b) ∈m mbindd U f t <-> (exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, 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

forall (A B : Type) (f : W * A ~k~> T B) (t : U A) (k2 : K) (b : B), (k2, b) ∈m mbindd U f t <-> (exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(k2, b) ∈m mbindd U f t <-> (exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(exists w : W, (w, (k2, b)) ∈md mbindd U f t) <-> (exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2) <-> (exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2) -> exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
(exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)) -> exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2) -> exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
wtotal: W
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (w2, (k2, b)) ∈md f k1 (w1, a)
hyp3: wtotal = w1 ● w2

exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
wtotal: W
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (w2, (k2, b)) ∈md f k1 (w1, a)
hyp3: wtotal = w1 ● w2

(w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
wtotal: W
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (w2, (k2, b)) ∈md f k1 (w1, a)
hyp3: wtotal = w1 ● w2

(k2, b) ∈m f k1 (w1, a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
wtotal: W
k1: K
w1, w2: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (k2, b) ∈m f k1 (w1, a)
hyp3: wtotal = w1 ● w2

(k2, b) ∈m f k1 (w1, 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, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B

(exists (k1 : K) (w1 : W) (a : A), (w1, (k1, a)) ∈md t /\ (k2, b) ∈m f k1 (w1, a)) -> exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: (k2, b) ∈m f k1 (w1, a)

exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1: W
a: A
hyp1: (w1, (k1, a)) ∈md t
hyp2: exists w : W, (w, (k2, b)) ∈md f k1 (w1, a)

exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1: W
a: A
hyp1: (w1, (k1, a)) ∈md t
w2: W
rest: (w2, (k2, b)) ∈md f k1 (w1, a)

exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: W * A ~k~> T B
t: U A
k2: K
b: B
k1: K
w1: W
a: A
hyp1: (w1, (k1, a)) ∈md t
w2: W
rest: (w2, (k2, b)) ∈md f k1 (w1, a)

(w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md f k1 (w1, a) /\ w1 ● w2 = w1 ● w2
intuition. Qed. (** *** Corollaries for other operations *) (********************************************************************)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : A ~k~> T B) (t : U A) (k2 : K) (b : B), (k2, b) ∈m mbind U f t <-> (exists (k1 : K) (a : A), (k1, a) ∈m t /\ (k2, b) ∈m f k1 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

forall (A B : Type) (f : A ~k~> T B) (t : U A) (k2 : K) (b : B), (k2, b) ∈m mbind U f t <-> (exists (k1 : K) (a : A), (k1, a) ∈m t /\ (k2, b) ∈m f k1 a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(k2, b) ∈m mbind U f t <-> (exists (k1 : K) (a : A), (k1, a) ∈m t /\ (k2, b) ∈m f k1 a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(k2, b) ∈m mbindd U (f ◻ allK extract) t <-> (exists (k1 : K) (a : A), (k1, a) ∈m t /\ (k2, b) ∈m f k1 a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists w : W, (w, (k2, b)) ∈md mbindd U (f ◻ allK extract) t) <-> (exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2) <-> (exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2) <-> (exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2) -> exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a)
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B
(exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a)) -> exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2) -> exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a)
firstorder.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B

(exists (k1 : K) (a : A), (exists w : W, (w, (k1, a)) ∈md t) /\ (exists w : W, (w, (k2, b)) ∈md f k1 a)) -> exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: A ~k~> T B
t: U A
k2: K
b: B
k1: K
a: A
w1: W
hyp1: (w1, (k1, a)) ∈md t
w: W
hyp2: (w, (k2, b)) ∈md f k1 a

exists (w : W) (k1 : K) (w1 w2 : W) (a : A), (w1, (k1, a)) ∈md t /\ (w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\ w = w1 ● w2
repeat eexists; eauto. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : K -> W * A -> B) (t : U A) (k : K) (b : B), (k, b) ∈m mmapd U f t <-> (exists (w : W) (a : A), (w, (k, a)) ∈md t /\ b = f 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

forall (A B : Type) (f : K -> W * A -> B) (t : U A) (k : K) (b : B), (k, b) ∈m mmapd U f t <-> (exists (w : W) (a : A), (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
b: B

(k, b) ∈m mmapd U f t <-> (exists (w : W) (a : A), (w, (k, a)) ∈md t /\ b = f k (w, a))
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T
A, B: Type
f: K -> W * A -> B
t: U A
k: K
b: B

(exists w : W, (w, (k, b)) ∈md mmapd U f t) <-> (exists (w : W) (a : A), (w, (k, a)) ∈md t /\ b = f k (w, a))
now setoid_rewrite inmd_mmapd_iff. Qed.
U: Type -> Type
ix: Index
W: Type
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind W T U
H: forall k : K, MBind W T (T k)
mn_op: Monoid_op W
mn_unit: Monoid_unit W
H0: MultiDecoratedTraversablePreModule W T U
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad W T

forall (A B : Type) (f : K -> A -> B) (t : U A) (k : K) (b : B), (k, b) ∈m mmap U f t <-> (exists a : A, (k, a) ∈m t /\ b = f 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

forall (A B : Type) (f : K -> A -> B) (t : U A) (k : K) (b : B), (k, b) ∈m mmap U f t <-> (exists a : A, (k, a) ∈m t /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
b: B

(k, b) ∈m mmap U f t <-> (exists a : A, (k, a) ∈m t /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
b: B

(exists w : W, (w, (k, b)) ∈md mmap U f t) <-> (exists a : A, (exists w : W, (w, (k, a)) ∈md t) /\ b = f 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, B: Type
f: K -> A -> B
t: U A
k: K
b: B

(exists (w : W) (a : A), (w, (k, a)) ∈md t /\ b = f k a) <-> (exists a : A, (exists w : W, (w, (k, a)) ∈md t) /\ b = f k a)
firstorder. Qed. End DTM_membership.