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 VariablesA B C F G W T U K.(** * Sorted lists with context *)(**********************************************************************)Sectionlist.Context
`{ix: Index}
`{Monoid W}.Instance: MReturn (funkA => list (W * (K * A))) :=
funA (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>>. *)Fixpointmbinddt_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 (AB : 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 (AB : 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 (AB : 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 (AB : 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)
nowrewrite (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 (AB : 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 (AB : 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 (AB : Type)
(f : K -> W * A -> list (W * (K * B)))
(l1l2 : 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 (AB : Type)
(f : K -> W * A -> list (W * (K * B)))
(l1l2 : 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
nowrewrite List.app_assoc.Qed.
ix: Index W: Type op: Monoid_op W unit0: Monoid_unit W H: Monoid W
forall (AB : 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 (AB : 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))
foralla1a2 : 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))
foralla1a2 : 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.Endlist.(** * Shape and Contents *)(**********************************************************************)(** ** Operations *)(**********************************************************************)Sectionshape_and_contents.Context
(U: Type -> Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}.Definitionshape {A}: U A -> U unit :=
mmap U (allK (const tt)).Definitiontolistmd_gen_loc {A}:
K -> W * A -> list (W * (K * A)) :=
funk '(w, a) => [(w, (k, a))].Definitiontolistmd_gen {A} (fake: Type):
U A -> list (W * (K * A)) :=
mmapdt (B := fake) U (const (list (W * (K * A))))
tolistmd_gen_loc.Definitiontolistmd {A}:
U A -> list (W * (K * A)) :=
tolistmd_gen False.Definitiontosetmd {A}:
U A -> W * (K * A) -> Prop :=
tosubset (F := list) ∘ tolistmd.Definitiontolistm {A}:
U A -> list (K * A) :=
map (F := list) extract ∘ tolistmd.Definitiontosetm {A}: U A -> K * A -> Prop :=
tosubset (F := list) ∘ tolistm.Fixpointfilterk {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.Definitiontoklistd {A} (k: K): U A -> list (W * A) :=
filterk k ∘ tolistmd.Definitiontoksetd {A} (k: K): U A -> W * A -> Prop :=
tosubset (F := list) ∘ toklistd k.Definitiontoklist {A} (k: K): U A -> list A :=
map (F := list) extract ∘ @toklistd A k.Endshape_and_contents.(** ** Notations *)(**********************************************************************)ModuleNotations.Notation"x ∈md t" :=
(tosetmd _ t x) (at level50): tealeaves_multi_scope.Notation"x ∈m t" :=
(tosetm _ t x) (at level50): tealeaves_multi_scope.EndNotations.Import Notations.(** ** Rewriting Rules for <<filterk>> *)(**********************************************************************)Sectionrw_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
foralllwa,
filterk k ((w, (k, a)) :: l) = (w, a) :: filterk k l
ix: Index W, A: Type k: K
foralllwa,
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
foralllwa (j : K),
j <> k -> filterk k ((w, (j, a)) :: l) = filterk k l
ix: Index W, A: Type k: K
foralllwa (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
foralll1l2,
filterk k (l1 ++ l2) = filterk k l1 ++ filterk k l2
ix: Index W, A: Type k: K
foralll1l2,
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
nowrewrite <- 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.Endrw_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*)(**********************************************************************)Sectionlemmas.#[local] Generalizable VariableM.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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M) f =
mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M) f =
mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M) f =
map (mmap U (const exfalso))
∘ mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M) f =
mbinddt U (const M)
(funk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M)
(f : forallk : K, W * A -> const M (T k fake1)) =
mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M)
(f : forallk : K, W * A -> const M (T k fake1)) =
mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : K, W * A -> const M (T k B)
mbinddt U (const M)
(f : forallk : K, W * A -> const M (T k fake1)) =
mbinddt U (const M)
(f : forallk : 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: forallk : K, 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: forallk : 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: forallk : K, 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: forallk : 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: forallk : K, MBind W T (T k) mn_op: Monoid_op W mn_unit: Monoid_unit W H0: MultiDecoratedTraversablePreModule W T U MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
W T
forallfakeA : 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: forallk : K, MBind W T (T k) mn_op: Monoid_op W mn_unit: Monoid_unit W H0: MultiDecoratedTraversablePreModule W T U MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
W T
forallfakeA : 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: forallk : K, 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: forallk : K, 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)
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind W T (T k) mn_op: Monoid_op W mn_unit: Monoid_unit W H0: MultiDecoratedTraversablePreModule W T U MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
W T
forallfake1fake2A : 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: forallk : K, MBind W T (T k) mn_op: Monoid_op W mn_unit: Monoid_unit W H0: MultiDecoratedTraversablePreModule W T U MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
W T
forallfake1fake2A : 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: forallk : K, 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: forallk : K, 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: forallk : K, 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.Endlemmas.(** ** Relating <<∈m>> and <<∈md>> *)(**********************************************************************)SectionDTM_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: forallk : K, 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 <-> (existsw : 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: forallk : K, 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 <-> (existsw : 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: forallk : K, 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 <-> (existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) <->
(existsw : 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: forallk : K, 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) Hfst: {{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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W Hrest: 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest1: {{(w', (k', a'))}} (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest2: tosubset l (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) Hfst: {{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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W Hrest: 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W Hrest: tosubset l (w, (k, a))
({{(w', (k', a'))}} ∪ tosubset l) (w, (k, a))
nowright.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest1: {{(w', (k', a'))}} (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest1: (w', (k', a')) = (w, (k, a))
{{extract (w', (k', a'))}} (k, a)
nowinversion rest1.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest2: tosubset l (w, (k, a))
{{extract (w', (k', a'))}} (k, a) \/
(existsw : 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: forallk : K, 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) <->
(existsw : W, tosubset l (w, (k, a))) w: W rest2: tosubset l (w, (k, a))
existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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) <->
(existsw : 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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
existsw : W, (w, (k, a)) ∈md t
eauto.Qed.EndDTM_membership_lemmas.(** ** Characterizing Membership in List Operations *)(**********************************************************************)SectionDTM_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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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)
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
nowleft.
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
nowright.}
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
nowright.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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 <->
(existsa0 : 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: forallk : K, MBind 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 ->
existsa0 : 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: forallk : K, MBind 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
(existsa0 : 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: forallk : K, MBind 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 ->
existsa0 : 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: forallk : K, MBind 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
existsa0 : 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: forallk : K, MBind 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: existsw : W, (w, (k, a)) ∈md t
existsa0 : 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: forallk : K, MBind 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
existsa0 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
(existsa0 : 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: forallk : K, MBind 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: forallk : K, MBind 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
existsw : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
nowsubst.Qed.EndDTM_tolist.(** ** Interaction between <<tolistmd>> and <<mret>>/<<mbindd>> *)(**********************************************************************)SectionDTM_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: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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))]
nowrewrite mmapdt_comp_mret.Qed.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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: forallk : K, 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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 (fakeAB : 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: forallk : K, 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 (fakeAB : 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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))))
((funk : 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: forallk : K, 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))))
((funk : 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: forallk : K, 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))) =
(funk : 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: forallk : K, 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)) =
((funk : 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: forallk : K, 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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: forallk : K, 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: forallk : K, 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: forallk : K, 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)))): forallf : forallk : 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))))
((funk : 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: forallk : K, 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)))): forallf : forallk : 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))))
((funk : 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))))
((funk : 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: forallk : K, 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)))): forallf : forallk : 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))))
((funk : K => const (map (incr w)) (T k fake))
◻ f)
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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.EndDTM_tolist.(** ** Characterizing Occurrences Post-Operation *)(**********************************************************************)SectionDTM_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: forallk : K, 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) (a1a2 : A) (k1k2 : 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: forallk : K, 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) (a1a2 : A) (k1k2 : 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: forallk : K, MBind 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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
nowsubst.Qed.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) (a1a2 : A) (k1k2 : 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: forallk : K, 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) (a1a2 : A) (k1k2 : 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: forallk : K, MBind 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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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) (a1a2 : 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: forallk : K, 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) (a1a2 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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) (a1a2 : A) (kj : 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: forallk : K, 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) (a1a2 : A) (kj : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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) (a1a2 : 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: forallk : K, 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) (a1a2 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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) (a1a2 : A) (kj : 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: forallk : K, 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) (a1a2 : A) (kj : 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: forallk : K, MBind 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: forallk : K, MBind 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
(existsw : 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: forallk : K, MBind 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
(existsw : 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: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w3 : 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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))
nowleft.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w3 : 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w3 : 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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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)
(w1w2 : W)
(a : A),
tosubset l (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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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 (AB : Type) (f : W * A ~k~> T B) (t : U A)
(k2 : K) (wtotal : W) (b : B),
(exists (k1 : K) (w1w2 : 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: forallk : K, 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 (AB : Type) (f : W * A ~k~> T B) (t : U A)
(k2 : K) (wtotal : W) (b : B),
(exists (k1 : K) (w1w2 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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))
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, 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 (AB : 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\
wtotal = w1 ● w2) <->
(exists (k1 : K) (w1w2 : 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: forallk : K, 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 (AB : Type) (f : K -> W * A -> B) (t : U A)
(k : K) (w : W) (b : B),
(w, (k, b)) ∈md mmapd U f t <->
(existsa : 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: forallk : K, 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 (AB : Type) (f : K -> W * A -> B) (t : U A)
(k : K) (w : W) (b : B),
(w, (k, b)) ∈md mmapd U f t <->
(existsa : 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: forallk : K, MBind 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 <->
(existsa : 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: forallk : K, MBind 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 <->
(existsa : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2, (k, b)) ∈md (mret T ◻ f) k1 (w1, a) /\
w = w1 ● w2) <->
(existsa : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2, (k, b)) ∈md (mret T ◻ f) k1 (w1, a) /\
w = w1 ● w2) <->
(existsa : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\
w = w1 ● w2) <->
(existsa : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\
w = w1 ● w2) ->
existsa : 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: forallk : K, MBind 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
(existsa : A, (w, (k, a)) ∈md t /\ b = f k (w, a)) ->
exists (k1 : K)
(w1w2 : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2 = Ƶ /\ k1 = k /\ f k1 (w1, a) = b) /\
w = w1 ● w2) ->
existsa : 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: forallk : K, MBind 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
existsa : 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: forallk : K, MBind 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
existsa0 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
(existsa : A, (w, (k, a)) ∈md t /\ b = f k (w, a)) ->
exists (k1 : K) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, 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 (AB : Type) (f : K -> A -> B) (t : U A)
(k : K) (w : W) (b : B),
(w, (k, b)) ∈md mmap U f t <->
(existsa : 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: forallk : K, 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 (AB : Type) (f : K -> A -> B) (t : U A)
(k : K) (w : W) (b : B),
(w, (k, b)) ∈md mmap U f t <->
(existsa : 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: forallk : K, MBind 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 <->
(existsa : 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: forallk : K, MBind 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 <->
(existsa : 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: forallk : K, MBind 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
(existsa : A,
(w, (k, a)) ∈md t /\
b = (f ◻ allK extract) k (w, a)) <->
(existsa : 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: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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
(existsw : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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: existsw : W, (w, (k2, b)) ∈md f k1 (w1, a)
exists (w : W) (k1 : K) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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: forallk : K, MBind 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: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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: forallk : K, MBind 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
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, MBind 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) (w1w2 : 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : 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: forallk : K, MBind 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) (w1w2 : 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : 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: forallk : K, MBind 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) (w1w2 : 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : 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: forallk : K, MBind 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : W, (w, (k2, b)) ∈md f k1 a)) ->
exists (w : W)
(k1 : K) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : 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: forallk : K, MBind 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),
(existsw : W, (w, (k1, a)) ∈md t) /\
(existsw : W, (w, (k2, b)) ∈md f k1 a)) ->
exists (w : W) (k1 : K) (w1w2 : 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: forallk : K, MBind 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) (w1w2 : W) (a : A),
(w1, (k1, a)) ∈md t /\
(w2, (k2, b)) ∈md (f ◻ allK extract) k1 (w1, a) /\
w = w1 ● w2
repeateexists; eauto.Qed.
U: Type -> Type ix: Index W: Type T: K -> Type -> Type MReturn0: MReturn T MBind0: MBind W T U H: forallk : K, 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 (AB : 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: forallk : K, 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 (AB : 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: forallk : K, MBind 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: forallk : K, MBind 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
(existsw : W, (w, (k, b)) ∈md mmapd U f t) <->
(exists (w : W) (a : A),
(w, (k, a)) ∈md t /\ b = f k (w, a))
nowsetoid_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: forallk : K, 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 (AB : Type) (f : K -> A -> B) (t : U A)
(k : K) (b : B),
(k, b) ∈m mmap U f t <->
(existsa : 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: forallk : K, 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 (AB : Type) (f : K -> A -> B) (t : U A)
(k : K) (b : B),
(k, b) ∈m mmap U f t <->
(existsa : 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: forallk : K, MBind 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 <->
(existsa : 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: forallk : K, MBind 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
(existsw : W, (w, (k, b)) ∈md mmap U f t) <->
(existsa : A,
(existsw : 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: forallk : K, MBind 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) <->
(existsa : A,
(existsw : W, (w, (k, a)) ∈md t) /\ b = f k a)