From Tealeaves Require Export
  Classes.Kleisli.ContainerMonad
  Classes.Kleisli.TraversableMonad
  Classes.Coalgebraic.TraversableFunctor
  Classes.Coalgebraic.TraversableMonad
  Adapters.KleisliToCoalgebraic.TraversableMonad
  Kleisli.Theory.TraversableMonad
  Theory.TraversableFunctor.

#[local] Generalizable Variables U T G A B C ϕ M.

Import Monoid.Notations.
Import Applicative.Notations.
Import TraversableFunctor.Notations.
Import TraversableMonad.Notations.
Import ContainerFunctor.Notations.
Import Subset.Notations.

Import Kleisli.TraversableMonad.DerivedInstances.



(** * Simultaneous Induction on Two <<Batch>>es of the Same Length *)
(******************************************************************************)
Section shape_induction.

  Context
    {A1 A2 B1 B2 C D: Type}
      {b1: Batch A1 B1 C}
      {b2: Batch A2 B2 D}
      (Hshape: length_Batch b1 = length_Batch b2)
      (P : forall C D : Type,
          Batch A1 B1 C ->
          Batch A2 B2 D ->
          Prop)
      (IHdone:
        forall (C D : Type) (c : C) (d: D), P C D (Done c) (Done d))
      (IHstep:
        forall (C D : Type)
          (b1 : Batch A1 B1 (B1 -> C))
          (b2 : Batch A2 B2 (B2 -> D)),
          P (B1 -> C) (B2 -> D) b1 b2 ->
          forall (a1 : A1) (a2: A2)
            (Hshape: length_Batch (Step b1 a1) =
                       length_Batch (Step b2 a2)),
            P C D (Step b1 a1) (Step b2 a2)).

  Lemma Batch_length_ind: P C D b1 b2.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
b2: Batch A2 B2 D
Hshape: length_Batch b1 = length_Batch b2
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
P C D b1 b2
  Proof.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
b2: Batch A2 B2 D
Hshape: length_Batch b1 = length_Batch b2
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
P C D b1 b2
    generalize dependent Hshape.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
b2: Batch A2 B2 D
Hshape: length_Batch b1 = length_Batch b2
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
length_Batch b1 = length_Batch b2 -> P C D b1 b2
    generalize dependent b2.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
b2: Batch A2 B2 D
Hshape: length_Batch b1 = length_Batch b2
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
forall b2 : Batch A2 B2 D,
length_Batch b1 = length_Batch b2 ->
length_Batch b1 = length_Batch b2 -> P C D b1 b2
    clear Hshape.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
b2: Batch A2 B2 D
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
forall b2 : Batch A2 B2 D,
length_Batch b1 = length_Batch b2 ->
length_Batch b1 = length_Batch b2 -> P C D b1 b2
    clear b2.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
forall b2 : Batch A2 B2 D,
length_Batch b1 = length_Batch b2 ->
length_Batch b1 = length_Batch b2 -> P C D b1 b2
    generalize dependent D.
A1, A2, B1, B2, C, D: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch b1 = length_Batch b2 ->
length_Batch b1 = length_Batch b2 -> P C D b1 b2
    induction b1 as [C c | C rest IHrest a];
      intros D0 b2 Hshape ?.
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
Hshape, Hshape0: length_Batch (Done c) = length_Batch b2
P C D0 (Done c) b2
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
Hshape, Hshape0: length_Batch (Step rest a) = length_Batch b2
P C D0 (Step rest a) b2
    -
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
Hshape, Hshape0: length_Batch (Done c) = length_Batch b2
P C D0 (Done c) b2 destruct b2.
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
d: D0
Hshape, Hshape0: length_Batch (Done c) =
length_Batch (Done d)
P C D0 (Done c) (Done d)
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
b: Batch A2 B2 (B2 -> D0)
a: A2
Hshape, Hshape0: length_Batch (Done c) =
length_Batch (Step b a)
P C D0 (Done c) (Step b a)
      +
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
d: D0
Hshape, Hshape0: length_Batch (Done c) =
length_Batch (Done d)
P C D0 (Done c) (Done d) now inversion Hshape.
      +
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
c: C
D0: Type
b2: Batch A2 B2 D0
b: Batch A2 B2 (B2 -> D0)
a: A2
Hshape, Hshape0: length_Batch (Done c) =
length_Batch (Step b a)
P C D0 (Done c) (Step b a) false.
    -
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
Hshape, Hshape0: length_Batch (Step rest a) = length_Batch b2
P C D0 (Step rest a) b2 destruct b2 as [c' | rest' a'].
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
c': D0
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Done c')
P C D0 (Step rest a) (Done c')
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
P C D0 (Step rest a) (Step rest' a')
      +
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
c': D0
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Done c')
P C D0 (Step rest a) (Done c') false.
      +
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
P C D0 (Step rest a) (Step rest' a') apply IHstep.
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
P (B1 -> C) (B2 -> D0) rest rest'
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
length_Batch (Step rest a) =
length_Batch (Step rest' a')
        *
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
P (B1 -> C) (B2 -> D0) rest rest' specialize (IHrest rest).
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
P (B1 -> C) (B2 -> D0) rest rest'
          inversion Hshape.
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
H0: length_Batch rest = length_Batch rest'
P (B1 -> C) (B2 -> D0) rest rest'
          apply IHrest; auto.
        *
A1, A2, B1, B2, D, C: Type
b1: Batch A1 B1 C
P: forall C D : Type,
Batch A1 B1 C -> Batch A2 B2 D -> Prop
IHdone: forall (C D : Type) (c : C) (d : D),
P C D (Done c) (Done d)
IHstep: forall (C D : Type)
  (b1 : Batch A1 B1 (B1 -> C))
  (b2 : Batch A2 B2 (B2 -> D)),
P (B1 -> C) (B2 -> D) b1 b2 ->
forall (a1 : A1) (a2 : A2),
length_Batch (Step b1 a1) =
length_Batch (Step b2 a2) ->
P C D (Step b1 a1) (Step b2 a2)
rest: Batch A1 B1 (B1 -> C)
a: A1
IHrest: Batch A1 B1 (B1 -> C) ->
forall (D : Type) (b2 : Batch A2 B2 D),
length_Batch rest = length_Batch b2 ->
length_Batch rest = length_Batch b2 ->
P (B1 -> C) D rest b2
D0: Type
b2: Batch A2 B2 D0
rest': Batch A2 B2 (B2 -> D0)
a': A2
Hshape, Hshape0: length_Batch (Step rest a) =
length_Batch (Step rest' a')
length_Batch (Step rest a) =
length_Batch (Step rest' a') assumption.
  Qed.

End shape_induction.

(*
(** ** Simultaneous Induction but now D is monomorphic *)
(******************************************************************************)
Section shape_induction.

  Context
    {A1 A2 B1 B2 C D: Type}
      {b1: Batch A1 B1 C}
      {b2: Batch A2 B2 D}
      (Hshape: length_Batch b1 = length_Batch b2)
      (P :Batch A1 B1 C ->
          Batch A2 B2 D ->
          Prop)
      (IHdone:
        forall (c : C) (d: D), P (Done c) (Done d))
      (IHstep:
        forall (b1 : Batch A1 B1 (B1 -> C))
          (b2 : Batch A2 B2 (B2 -> D)),
          P (B1 -> C) (B2 -> D) b1 b2 ->
          forall (a1 : A1) (a2: A2)
            (Hshape: length_Batch (Step b1 a1) =
                       length_Batch (Step b2 a2)),
            P C D (Step b1 a1) (Step b2 a2)).

  Lemma Batch_length_ind: P C D b1 b2.
  Proof.
    generalize dependent Hshape.
    generalize dependent b2.
    clear Hshape.
    clear b2.
    generalize dependent D.
    induction b1 as [C c | C rest IHrest a];
      intros D0 b2 Hshape ?.
    - destruct b2.
      + now inversion Hshape.
      + false.
    - destruct b2 as [c' | rest' a'].
      + false.
      + apply IHstep.
        * specialize (IHrest rest).
          inversion Hshape.
          apply IHrest; auto.
        * assumption.
  Qed.

End shape_induction.
*)


(** * Theory of Traversable Monads *)
(**********************************************************************)
Section traversable_monad_theory.

  Context
    `{ret_inst: Return T}
    `{Map_T_inst: Map T}
    `{Traverse_T_inst: Traverse T}
    `{Bind_T_inst: Bind T T}
    `{Bindt_T_inst: Bindt T T}
    `{ToSubset_T_inst: ToSubset T}
    `{ToBatch_T_inst: ToBatch T}
    `{ToBatch6_T_inst: ToBatch6 T T}
    `{! Compat_Map_Bindt T T}
    `{! Compat_Traverse_Bindt T T}
    `{! Compat_Bind_Bindt T T}
    `{! Compat_ToSubset_Traverse T}
    `{! Compat_ToBatch_Traverse T}
    `{! Compat_ToBatch6_Bindt T T}.

  Context
    `{Map_U_inst: Map U}
    `{Traverse_U_inst: Traverse U}
    `{Bind_U_inst: Bind T U}
    `{Bindt_U_inst: Bindt T U}
    `{ToSubset_U_inst: ToSubset U}
    `{ToBatch_U_inst: ToBatch U}
    `{ToBatch6_U_inst: ToBatch6 T U}
    `{! Compat_Map_Bindt T U}
    `{! Compat_Traverse_Bindt T U}
    `{! Compat_Bind_Bindt T U}
    `{! Compat_ToSubset_Traverse U}
    `{! Compat_ToBatch_Traverse U}
    `{! Compat_ToBatch6_Bindt T U}.


  Context
    `{Monad_inst: ! TraversableMonad T}
    `{Module_inst: ! TraversableRightPreModule T U}.

  (** ** Factoring operations through <<toBatch>> *)
  (********************************************************************)
  Section runBatch.

    Lemma bindt_through_runBatch6 `{Applicative G} `(f: A -> G (T B)):
      bindt (U := U) f = runBatch f ∘ toBatch6 (B := B).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = runBatch f ∘ toBatch6
    Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = runBatch f ∘ toBatch6
      intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = runBatch f ∘ toBatch6
      rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = runBatch f ∘ bindt (batch A (T B))
      rewrite (ktm_morph (ϕ := @runBatch _ _ G _ _ _ f)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = bindt (runBatch f ∘ batch A (T B))
      rewrite (runBatch_batch G).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G (T B)
bindt f = bindt f
      reflexivity.
    Qed.

    Corollary bind_through_runBatch6 `{Applicative G} `(f: A -> T B):
      bind (U := U) f = runBatch (G := fun A => A) f ∘ toBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
bind f = runBatch f ∘ toBatch6
    Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
bind f = runBatch f ∘ toBatch6
      rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
bind f = runBatch f ∘ bindt (batch A (T B))
      rewrite bind_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
bindt f = runBatch f ∘ bindt (batch A (T B))
      rewrite bindt_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
runBatch f ∘ toBatch6 =
runBatch f ∘ bindt (batch A (T B))
      rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> T B
runBatch f ∘ bindt (batch A (T B)) =
runBatch f ∘ bindt (batch A (T B))
      reflexivity.
    Qed.

    Corollary traverse_through_runBatch6 `{Applicative G} `(f: A -> G B):
      traverse (T := U) f = runBatch (map ret ∘ f) ∘ toBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f = runBatch (map ret ∘ f) ∘ toBatch6
    Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f = runBatch (map ret ∘ f) ∘ toBatch6
      rewrite traverse_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
bindt (map ret ∘ f) =
runBatch (map ret ∘ f) ∘ toBatch6
      rewrite bindt_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
runBatch (map ret ∘ f) ∘ toBatch6 =
runBatch (map ret ∘ f) ∘ toBatch6
      reflexivity.
    Qed.

    Corollary map_through_runBatch6 `(f: A -> B):
      map (F := U) f = runBatch (G := fun A => A) (ret (T := T) ∘ f) ∘ toBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
map f = runBatch (ret ∘ f) ∘ toBatch6
    Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
map f = runBatch (ret ∘ f) ∘ toBatch6
      rewrite map_to_traverse.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
traverse f = runBatch (ret ∘ f) ∘ toBatch6
      rewrite traverse_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
runBatch (map ret ∘ f) ∘ toBatch6 =
runBatch (ret ∘ f) ∘ toBatch6
      reflexivity.
    Qed.

    Corollary id_through_runBatch6: forall (A: Type),
        id (A := U A) = runBatch (G := fun A => A) (ret (T := T)) ∘ toBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, id = runBatch ret ∘ toBatch6
    Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall A : Type, id = runBatch ret ∘ toBatch6
      intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
id = runBatch ret ∘ toBatch6
      rewrite <- (fun_map_id (F := U)).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
map id = runBatch ret ∘ toBatch6
      rewrite map_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A: Type
runBatch (ret ∘ id) ∘ toBatch6 =
runBatch ret ∘ toBatch6
      reflexivity.
    Qed.

    (** ** Relating <<toBatch6>> with <<toBatch>> *)
    (******************************************************************)
    Lemma toBatch6_toBatch
      {A B: Type} (t: U A):
      toBatch (A' := B) t = mapsnd_Batch (ret (T := T)) (toBatch6 t).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
toBatch t = mapsnd_Batch ret (toBatch6 t)
      Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
toBatch t = mapsnd_Batch ret (toBatch6 t)
        intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
toBatch t = mapsnd_Batch ret (toBatch6 t)
        rewrite toBatch_to_traverse.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
traverse (batch A B) t = mapsnd_Batch ret (toBatch6 t)
        rewrite traverse_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
bindt (map ret ∘ batch A B) t =
mapsnd_Batch ret (toBatch6 t)
        rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
bindt (map ret ∘ batch A B) t =
mapsnd_Batch ret (bindt (batch A (T B)) t)
        compose near t on right.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
bindt (map ret ∘ batch A B) t =
(mapsnd_Batch ret ∘ bindt (batch A (T B))) t
        rewrite (ktm_morph (G1 := Batch A (T B)) (G2 := Batch A B)
                   (ϕ := fun C => mapsnd_Batch (ret (T := T)))).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
bindt (map ret ∘ batch A B) t =
bindt (mapsnd_Batch ret ∘ batch A (T B)) t
        rewrite ret_dinatural.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
bindt (map ret ∘ batch A B) t =
bindt (map ret ∘ batch A B) t
        reflexivity.
      Qed.

  End runBatch.

  (** ** Naturality of <<toBatch6>> *)
  (********************************************************************)
  Lemma toBatch6_mapfst
    {A B: Type} (f: A -> B) {C: Type}:
    toBatch6 (B := C) ∘ map (F := U) f =
      mapfst_Batch f ∘ toBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
toBatch6 ∘ map f = mapfst_Batch f ∘ toBatch6
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
toBatch6 ∘ map f = mapfst_Batch f ∘ toBatch6
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
toBatch6 ∘ map f = mapfst_Batch f ∘ toBatch6
    rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
bindt (batch B (T C)) ∘ map f =
mapfst_Batch f ∘ toBatch6
    rewrite (bindt_map (G2 := Batch B (T C))).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
bindt (batch B (T C) ∘ f) = mapfst_Batch f ∘ toBatch6
    rewrite (bindt_through_runBatch6 (G := Batch B (T C))).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
runBatch (batch B (T C) ∘ f) ∘ toBatch6 =
mapfst_Batch f ∘ toBatch6
    rewrite toBatch6_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
runBatch (batch B (T C) ∘ f) ∘ bindt (batch A (T C)) =
mapfst_Batch f ∘ bindt (batch A (T C))
    rewrite (bindt_through_runBatch6 (G := Batch A (T C))).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
runBatch (batch B (T C) ∘ f)
∘ (runBatch (batch A (T C)) ∘ toBatch6) =
mapfst_Batch f ∘ (runBatch (batch A (T C)) ∘ toBatch6)
    ext t.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
(runBatch (batch B (T C) ∘ f)
 ∘ (runBatch (batch A (T C)) ∘ toBatch6)) t =
(mapfst_Batch f
 ∘ (runBatch (batch A (T C)) ∘ toBatch6)) t
    unfold compose.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) (toBatch6 t)) =
mapfst_Batch f (runBatch (batch A (T C)) (toBatch6 t))
    induction (toBatch6 t).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
c: C0
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) (Done c)) =
mapfst_Batch f (runBatch (batch A (T C)) (Done c))
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
IHb: runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) =
mapfst_Batch f (runBatch (batch A (T C)) b)
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) (Step b a)) =
mapfst_Batch f (runBatch (batch A (T C)) (Step b a))
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
c: C0
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) (Done c)) =
mapfst_Batch f (runBatch (batch A (T C)) (Done c)) cbn.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
c: C0
pure c = Done c reflexivity.
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
IHb: runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) =
mapfst_Batch f (runBatch (batch A (T C)) b)
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) (Step b a)) =
mapfst_Batch f (runBatch (batch A (T C)) (Step b a)) rewrite runBatch_rw2.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
IHb: runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) =
mapfst_Batch f (runBatch (batch A (T C)) b)
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a) =
mapfst_Batch f
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a)
      rewrite mapfst_Batch2.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
IHb: runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) =
mapfst_Batch f (runBatch (batch A (T C)) b)
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a) =
mapfst_Batch f (runBatch (batch A (T C)) b) <⋆>
mapfst_Batch f (batch A (T C) a)
      Set Keyed Unification.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
IHb: runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) =
mapfst_Batch f (runBatch (batch A (T C)) b)
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a) =
mapfst_Batch f (runBatch (batch A (T C)) b) <⋆>
mapfst_Batch f (batch A (T C) a)
      rewrite <- IHb; clear IHb.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a) =
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) <⋆>
mapfst_Batch f (batch A (T C) a)
      Unset Keyed Unification.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> B
C: Type
t: U A
C0: Type
b: Batch A (T C) (T C -> C0)
a: A
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b <⋆> batch A (T C) a) =
runBatch (batch B (T C) ○ f)
  (runBatch (batch A (T C)) b) <⋆>
mapfst_Batch f (batch A (T C) a)
  Abort. (* TODO *)

  (** ** Respectfulness properties *)
  (********************************************************************)
  Lemma bindt_respectful:
    forall (G: Type -> Type)
      `{Applicative G} `(f1: A -> G (T B)) `(f2: A -> G (T B)) (t: U A),
      (forall (a: A), a ∈ t -> f1 a = f2 a) ->
      bindt (U := U) f1 t = bindt f2 t.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f1 f2 : A -> G (T B)) (t : U A),
(forall a : A, a ∈ t -> f1 a = f2 a) ->
bindt f1 t = bindt f2 t
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f1 f2 : A -> G (T B)) (t : U A),
(forall a : A, a ∈ t -> f1 a = f2 a) ->
bindt f1 t = bindt f2 t
    introv ? hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A, a ∈ t -> f1 a = f2 a
bindt f1 t = bindt f2 t
    rewrite bindt_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A, a ∈ t -> f1 a = f2 a
(runBatch f1 ∘ toBatch6) t = bindt f2 t
    rewrite bindt_through_runBatch6.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A, a ∈ t -> f1 a = f2 a
(runBatch f1 ∘ toBatch6) t =
(runBatch f2 ∘ toBatch6) t
    unfold element_of in hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A, tosubset t a -> f1 a = f2 a
(runBatch f1 ∘ toBatch6) t =
(runBatch f2 ∘ toBatch6) t
    rewrite (tosubset_through_runBatch2 A B) in hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A,
(runBatch ret ∘ toBatch) t a -> f1 a = f2 a
(runBatch f1 ∘ toBatch6) t =
(runBatch f2 ∘ toBatch6) t
    unfold compose at 1 2.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A,
(runBatch ret ∘ toBatch) t a -> f1 a = f2 a
runBatch f1 (toBatch6 t) = runBatch f2 (toBatch6 t)
    unfold compose at 1 in hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A,
runBatch ret (toBatch t) a -> f1 a = f2 a
runBatch f1 (toBatch6 t) = runBatch f2 (toBatch6 t)
    setoid_rewrite toBatch6_toBatch in hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A,
runBatch ret (mapsnd_Batch ret (toBatch6 t)) a ->
f1 a = f2 a
runBatch f1 (toBatch6 t) = runBatch f2 (toBatch6 t)
    rewrite <- runBatch_mapsnd in hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
hyp: forall a : A,
runBatch (map ret ∘ ret) (toBatch6 t) a ->
f1 a = f2 a
runBatch f1 (toBatch6 t) = runBatch f2 (toBatch6 t)
    induction (toBatch6 t).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
c: C
hyp: forall a : A,
runBatch (map ret ∘ ret) (Done c) a ->
f1 a = f2 a
runBatch f1 (Done c) = runBatch f2 (Done c)
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f1 (Step b a) = runBatch f2 (Step b a)
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
c: C
hyp: forall a : A,
runBatch (map ret ∘ ret) (Done c) a ->
f1 a = f2 a
runBatch f1 (Done c) = runBatch f2 (Done c) cbn in *.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
c: C
hyp: forall a : A, pure c a -> f1 a = f2 a
pure c = pure c
      reflexivity.
    -
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f1 (Step b a) = runBatch f2 (Step b a) cbn.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f1 b <⋆> f1 a = runBatch f2 b <⋆> f2 a
      rewrite IHb.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f2 b <⋆> f1 a = runBatch f2 b <⋆> f2 a
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
forall a : A,
runBatch (map ret ∘ ret) b a -> f1 a = f2 a
      +
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f2 b <⋆> f1 a = runBatch f2 b <⋆> f2 a rewrite hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f2 b <⋆> f2 a = runBatch f2 b <⋆> f2 a
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch (map ret ∘ ret) (Step b a) a
        *
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch f2 b <⋆> f2 a = runBatch f2 b <⋆> f2 a reflexivity.
        *
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
runBatch (map ret ∘ ret) (Step b a) a cbn.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
(runBatch (map ret ∘ ret) b ● (map ret ∘ ret) a) a unfold compose.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
(runBatch (map ret ○ ret) b ● map ret (ret a)) a
          change (List.In ?a ?l) with (element_of (F := list) l a).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
(runBatch (map ret ○ ret) b ● map ret (ret a)) a
          unfold_ops @Monoid_op_list.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
(runBatch (map ret ○ ret) b ● map ret (ret a)) a
          autorewrite with tea_list.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
(runBatch (map ret ○ ret) b ● map ret (ret a)) a
          right.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
map ret (ret a) a
          reflexivity.
      +
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
forall a : A,
runBatch (map ret ∘ ret) b a -> f1 a = f2 a intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
f1 a0 = f2 a0 apply hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
runBatch (map ret ∘ ret) (Step b a) a0 cbn.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
(runBatch (map ret ∘ ret) b ● (map ret ∘ ret) a) a0
        change (List.In ?a ?l) with (element_of (F := list) l a).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
(runBatch (map ret ∘ ret) b ● (map ret ∘ ret) a) a0
        unfold_ops @Monoid_op_list.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
(runBatch (map ret ∘ ret) b ● (map ret ∘ ret) a) a0
        autorewrite with tea_list.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f1, f2: A -> G (T B)
t: U A
C: Type
b: Batch A (T B) (T B -> C)
a: A
hyp: forall a0 : A,
runBatch (map ret ∘ ret) (Step b a) a0 ->
f1 a0 = f2 a0
IHb: (forall a : A,
 runBatch (map ret ∘ ret) b a -> f1 a = f2 a) ->
runBatch f1 b = runBatch f2 b
a0: A
H0: runBatch (map ret ∘ ret) b a0
(runBatch (map ret ∘ ret) b ● (map ret ∘ ret) a) a0
        now left.
  Qed.

  Corollary bind_respectful:
    forall (A B: Type) (t: U A) (f1: A -> T B) `(f2: A -> T B),
      (forall (a: A), a ∈ t -> f1 a = f2 a) ->
      bind (U := U) f1 t = bind (U := U) f2 t.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (t : U A) (f1 f2 : A -> T B),
(forall a : A, a ∈ t -> f1 a = f2 a) ->
bind f1 t = bind f2 t
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (t : U A) (f1 f2 : A -> T B),
(forall a : A, a ∈ t -> f1 a = f2 a) ->
bind f1 t = bind f2 t
    introv hyp.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
f1, f2: A -> T B
hyp: forall a : A, a ∈ t -> f1 a = f2 a
bind f1 t = bind f2 t
    rewrite bind_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
f1, f2: A -> T B
hyp: forall a : A, a ∈ t -> f1 a = f2 a
bindt f1 t = bind f2 t
    rewrite bind_to_bindt.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: U A
f1, f2: A -> T B
hyp: forall a : A, a ∈ t -> f1 a = f2 a
bindt f1 t = bindt f2 t
    now apply (bindt_respectful (fun A => A) f1 f2).
  Qed.

  (** ** <<tosubset>> is a Homomorphism *)
  (********************************************************************)
  #[export] Instance tosubset_hom2_Module:
    ParallelRightModuleHom T subset U subset
      (@tosubset T _)
      (@tosubset U _).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
ParallelRightModuleHom T subset U subset
  (@tosubset T ToSubset_T_inst)
  (@tosubset U ToSubset_U_inst)
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
ParallelRightModuleHom T subset U subset
  (@tosubset T ToSubset_T_inst)
  (@tosubset U ToSubset_U_inst)
    constructor.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (f : A -> T B),
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
tosubset ∘ bind f = bind (tosubset ∘ f) ∘ tosubset
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce ret ∘ bind f =
bind (tosubset ∘ f) ∘ tosubset
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce ret ∘ bind f =
bind (mapReduce ret ∘ f) ∘ tosubset
    rewrite tosubset_to_mapReduce.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce ret ∘ bind f =
bind (mapReduce ret ∘ f) ∘ mapReduce ret
    rewrite mapReduce_bind.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce ret ∘ f) =
bind (mapReduce ret ∘ f) ∘ mapReduce ret
    rewrite (mapReduce_morphism (subset A) (subset B)
               (T := U)
               (ϕ := bind (mapReduce (ret (T := subset)) ∘ f))).
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce ret ∘ f) =
mapReduce (bind (mapReduce ret ∘ f) ∘ ret)
    rewrite set_bind0.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
f: A -> T B
mapReduce (mapReduce ret ∘ f) =
mapReduce (mapReduce ret ∘ f)
    reflexivity.
  Qed.

End traversable_monad_theory.

(** ** Monad Homomorphisms *)
(**********************************************************************)
Section homomorphisms.

  Context
    `{ret_inst: Return T}
    `{Map_T_inst: Map T}
    `{Traverse_T_inst: Traverse T}
    `{Bind_T_inst: Bind T T}
    `{Bindt_T_inst: Bindt T T}
    `{ToSubset_T_inst: ToSubset T}
    `{ToBatch_T_inst: ToBatch T}
    `{ToBatch6_T_inst: ToBatch6 T T}
    `{! Compat_Map_Bindt T T}
    `{! Compat_Traverse_Bindt T T}
    `{! Compat_Bind_Bindt T T}
    `{! Compat_ToSubset_Traverse T}
    `{! Compat_ToBatch_Traverse T}
    `{! Compat_ToBatch6_Bindt T T}.

  Context
    `{Map_U_inst: Map U}
    `{Traverse_U_inst: Traverse U}
    `{Bind_U_inst: Bind T U}
    `{Bindt_U_inst: Bindt T U}
    `{ToSubset_U_inst: ToSubset U}
    `{ToBatch_U_inst: ToBatch U}
    `{ToBatch6_U_inst: ToBatch6 T U}
    `{! Compat_Map_Bindt T U}
    `{! Compat_Traverse_Bindt T U}
    `{! Compat_Bind_Bindt T U}
    `{! Compat_ToSubset_Traverse U}
    `{! Compat_ToBatch_Traverse U}
    `{! Compat_ToBatch6_Bindt T U}.


  Context
    `{Monad_inst: ! TraversableMonad T}
    `{Module_inst: ! TraversableRightPreModule T U}.

  #[export] Instance Monad_Hom_Tolist
   : MonadHom T list (@tolist T _) :=
    {| kmon_hom_ret := tolist_ret;
       kmon_hom_bind := tolist_bind;
    |}.

  #[export] Instance Monad_Hom_Toset
   : MonadHom T subset (@tosubset T _) :=
    {| kmon_hom_ret := tosubset_hom1;
       kmon_hom_bind := tosubset_hom2;
    |}.

  #[export] Instance ContainerMonad_Traversable:
    ContainerMonad T.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
ContainerMonad T
  Proof.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
ContainerMonad T
    constructor; try typeclasses eauto.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
forall (A B : Type) (t : T A) (f g : A -> T B),
(forall a : A, a ∈ t -> f a = g a) ->
bind f t = bind g t
    intros.
T: Type -> Type
ret_inst: Return T
Map_T_inst: Map T
Traverse_T_inst: Traverse T
Bind_T_inst: Bind T T
Bindt_T_inst: Bindt T T
ToSubset_T_inst: ToSubset T
ToBatch_T_inst: ToBatch T
ToBatch6_T_inst: ToBatch6 T T
Compat_Map_Bindt0: Compat_Map_Bindt T T
Compat_Traverse_Bindt0: Compat_Traverse_Bindt T T
Compat_Bind_Bindt0: Compat_Bind_Bindt T T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Compat_ToBatch_Traverse0: Compat_ToBatch_Traverse T
Compat_ToBatch6_Bindt0: Compat_ToBatch6_Bindt T T
U: Type -> Type
Map_U_inst: Map U
Traverse_U_inst: Traverse U
Bind_U_inst: Bind T U
Bindt_U_inst: Bindt T U
ToSubset_U_inst: ToSubset U
ToBatch_U_inst: ToBatch U
ToBatch6_U_inst: ToBatch6 T U
Compat_Map_Bindt1: Compat_Map_Bindt T U
Compat_Traverse_Bindt1: Compat_Traverse_Bindt T U
Compat_Bind_Bindt1: Compat_Bind_Bindt T U
Compat_ToSubset_Traverse1: Compat_ToSubset_Traverse U
Compat_ToBatch_Traverse1: Compat_ToBatch_Traverse U
Compat_ToBatch6_Bindt1: Compat_ToBatch6_Bindt T U
Monad_inst: TraversableMonad T
Module_inst: TraversableRightPreModule T U
A, B: Type
t: T A
f, g: A -> T B
H: forall a : A, a ∈ t -> f a = g a
bind f t = bind g t now apply bind_respectful.
  Qed.

  #[export] Instance ContainerModule_Traversable:
    ContainerRightModule T U :=
        {| contmod_pointwise := bind_respectful;
           contmod_hom := tosubset_hom2_Module;
        |}.

End homomorphisms.