From Tealeaves Require Export
  Adapters.CategoricalToKleisli.TraversableFunctor
  Adapters.KleisliToCoalgebraic.TraversableFunctor
  Classes.Coalgebraic.TraversableFunctor
  Functors.Batch
  Functors.List
  Functors.VectorRefinement
  Theory.TraversableFunctor.

Import Coalgebraic.TraversableFunctor (ToBatch, toBatch).
Import KleisliToCoalgebraic.TraversableFunctor.DerivedInstances.

Import Subset.Notations.
Import Applicative.Notations.
Import ContainerFunctor.Notations.
Import ProductFunctor.Notations.
Import Kleisli.TraversableFunctor.Notations.
Import Batch.Notations.
Import Monoid.Notations.
Import VectorRefinement.Notations.

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

#[local] Arguments mapfst_Batch {B C A1 A2}%type_scope
  f%function_scope b.
#[local] Arguments mapsnd_Batch {A B1 B2 C}%type_scope
  f%function_scope b.




(** * Lifting relations over Traversable functors *)
(**********************************************************************)
Definition lift_relation {X} {A B:Type} `{Traverse X}
  (R: A -> B -> Prop): X A -> X B -> Prop :=
  traverse (G := subset) R.

Lemma lift_relation_rw {X} {A B:Type} `{Traverse X}
  (R: A -> B -> Prop) t1 t2:
  lift_relation R t1 t2 = traverse (G := subset) R t1 t2.
X: Type -> Type
A, B: Type
H: Traverse X
R: A -> B -> Prop
t1: X A
t2: X B
lift_relation R t1 t2 = traverse R t1 t2
Proof.
X: Type -> Type
A, B: Type
H: Traverse X
R: A -> B -> Prop
t1: X A
t2: X B
lift_relation R t1 t2 = traverse R t1 t2
  reflexivity.
Qed.

Section lifting_relations.

  Context
    `{Classes.Categorical.TraversableFunctor.TraversableFunctor T}.

  Import CategoricalToKleisli.TraversableFunctor.DerivedOperations.
  Import CategoricalToKleisli.TraversableFunctor.DerivedInstances.
  Import KleisliToCoalgebraic.TraversableFunctor.DerivedOperations.
  Import KleisliToCoalgebraic.TraversableFunctor.DerivedInstances.

  Context
    `{ToSubset T}
    `{! Compat_ToSubset_Traverse T}.

  Lemma relation_spec:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B),
      lift_relation R t u <->
        (exists b: Vector (plength t) B,
            traverse (G := subset) R (trav_contents t) b /\
              trav_make t b = u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B),
lift_relation R t u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B),
lift_relation R t u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
lift_relation R t u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    unfold lift_relation.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
traverse R t u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    rewrite traverse_repr.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
map (trav_make t)
  (forwards
     (traverse (mkBackwards ∘ R) (trav_contents t))) u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    compose near (trav_contents t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
map (trav_make t)
  ((forwards ∘ traverse (mkBackwards ∘ R))
     (trav_contents t)) u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    rewrite (traverse_commutative (G := subset) (T := Vector (plength t))).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
map (trav_make t) (traverse R (trav_contents t)) u <->
(exists b : Vector (plength t) B,
   traverse R (trav_contents t) b /\ trav_make t b = u)
    reflexivity.
  Qed.

  (* Minor, not helpful  *)
  Lemma relation1:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B)
      (Plen: plength u = plength t),
      lift_relation R t u ->
        trav_make t (coerce Plen in trav_contents u) = u.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Plen : plength u = plength t),
lift_relation R t u ->
trav_make t (coerce Plen in trav_contents u) = u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Plen : plength u = plength t),
lift_relation R t u ->
trav_make t (coerce Plen in trav_contents u) = u
    introv Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
Hrel: lift_relation R t u
trav_make t (coerce Plen in trav_contents u) = u
    rewrite relation_spec in Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
Hrel: exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\
  trav_make t b = u
trav_make t (coerce Plen in trav_contents u) = u
    destruct Hrel as [trav_contents_u [Htrav Hmake]].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
trav_make t (coerce Plen in trav_contents u) = u
    assert (Hcontents: trav_contents u ~~ trav_contents_u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
trav_contents u ~~ trav_contents_u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
trav_make t (coerce Plen in trav_contents u) = u
    {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
trav_contents u ~~ trav_contents_u apply trav_contents_unique in Hmake.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_contents_u ~~ trav_contents u
trav_contents u ~~ trav_contents_u
      symmetry.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_contents_u ~~ trav_contents u
proj1_sig trav_contents_u =
proj1_sig (trav_contents u) assumption. }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
trav_make t (coerce Plen in trav_contents u) = u
    rewrite <- Hmake.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
trav_make t (coerce Plen in trav_contents u) =
trav_make t trav_contents_u
    apply Vector_fun_sim_eq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
trav_make t ~!~ trav_make t
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
coerce Plen in trav_contents u ~~ trav_contents_u
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
trav_make t ~!~ trav_make t reflexivity.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Plen: plength u = plength t
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Hcontents: trav_contents u ~~ trav_contents_u
coerce Plen in trav_contents u ~~ trav_contents_u vector_sim.
  Qed.

  Lemma relation2:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B)
      (Hlen: plength u = plength t),
      lift_relation R t u ->
      traverse (G := subset) R
        (trav_contents t)
        (coerce Hlen in trav_contents u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hlen : plength u = plength t),
lift_relation R t u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hlen : plength u = plength t),
lift_relation R t u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
    introv Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Hrel: lift_relation R t u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
    rewrite relation_spec in Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Hrel: exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\
  trav_make t b = u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
    destruct Hrel as [trav_contents_u [Hrel Hmake]].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
    enough (Heq: coerce Hlen in trav_contents u =
                             trav_contents_u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Heq: coerce Hlen in trav_contents u = trav_contents_u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
coerce Hlen in trav_contents u = trav_contents_u
    {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Heq: coerce Hlen in trav_contents u = trav_contents_u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) rewrite Heq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
Heq: coerce Hlen in trav_contents u = trav_contents_u
traverse R (trav_contents t) trav_contents_u
      assumption. }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
coerce Hlen in trav_contents u = trav_contents_u
    apply Vector_sim_eq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
coerce Hlen in trav_contents u ~~ trav_contents_u
    vector_sim.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
trav_contents u ~~ trav_contents_u
    symmetry.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
proj1_sig trav_contents_u =
proj1_sig (trav_contents u)
    apply trav_contents_unique.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
trav_contents_u: Vector (plength t) B
Hrel: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
trav_make t trav_contents_u = u
    assumption.
  Qed.

  Lemma relation3:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B)
      (Hlen: plength u = plength t),
      trav_make (B := B) t ~!~ trav_make u ->
      traverse (G := subset) R
        (trav_contents t)
        (coerce Hlen in trav_contents u) ->
            lift_relation R t u.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hlen : plength u = plength t),
trav_make t ~!~ trav_make u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) ->
lift_relation R t u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hlen : plength u = plength t),
trav_make t ~!~ trav_make u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) ->
lift_relation R t u
    introv Htrav.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) ->
lift_relation R t u
    rewrite relation_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) ->
exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\ trav_make t b = u
    exists (coerce Hlen in trav_contents u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) /\
trav_make t (coerce Hlen in trav_contents u) = u split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
trav_make t (coerce Hlen in trav_contents u) = u
    assumption.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
trav_make t (coerce Hlen in trav_contents u) = u
    change u with (id u) at 3.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
trav_make t (coerce Hlen in trav_contents u) = id u
    rewrite id_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
trav_make t (coerce Hlen in trav_contents u) =
trav_make u (trav_contents u)
    apply Vector_fun_sim_eq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
trav_make t ~!~ trav_make u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
coerce Hlen in trav_contents u ~~ trav_contents u
    assumption.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hlen: plength u = plength t
Htrav: trav_make t ~!~ trav_make u
H3: traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
coerce Hlen in trav_contents u ~~ trav_contents u
    vector_sim.
  Qed.

  Lemma relation4:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B),
      lift_relation R t u ->
      (forall C, trav_make (B := C) t ~!~ trav_make u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B),
lift_relation R t u ->
forall C : Type, trav_make t ~!~ trav_make u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B),
lift_relation R t u ->
forall C : Type, trav_make t ~!~ trav_make u
    introv Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: lift_relation R t u
forall C : Type, trav_make t ~!~ trav_make u intro C.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: lift_relation R t u
C: Type
trav_make t ~!~ trav_make u
    rewrite relation_spec in Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\
  trav_make t b = u
C: Type
trav_make t ~!~ trav_make u
    destruct Hrel as [trav_contents_u [Htrav Hmake]].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
C: Type
trav_make t ~!~ trav_make u
    eapply trav_make_unique.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
trav_contents_u: Vector (plength t) B
Htrav: traverse R (trav_contents t) trav_contents_u
Hmake: trav_make t trav_contents_u = u
C: Type
trav_make t ?v = u
    eassumption.
  Qed.

  (** ** Related terms have the same shape *)
  (********************************************************************)
  Lemma relation_implies_shape:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B),
      lift_relation R t u -> shape t = shape u.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B), lift_relation R t u -> shape t = shape u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B), lift_relation R t u -> shape t = shape u
    introv Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: lift_relation R t u
shape t = shape u
    apply trav_same_shape_rev.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: lift_relation R t u
forall B0 : Type, trav_make t ~!~ trav_make u
    eapply relation4.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hrel: lift_relation R t u
lift_relation ?R t u
    eassumption.
  Qed.

  (** ** Related terms have a related zip *)
  (********************************************************************)
  Lemma Monoid_op_Opposite_and:
    Monoid_op_Opposite Monoid_op_and = and.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Monoid_op_Opposite Monoid_op_and = and
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
Monoid_op_Opposite Monoid_op_and = and
    ext P1 P2; propext; cbv; tauto.
  Qed.

  (* Hshape is trying to use Derived.Map_Traverse
     so pass (H := H) to ensure the right Map F is chosen *)
  Lemma relation_to_zipped:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B)
      (Hshape: shape (H := H) t = shape u),
      lift_relation R t u ->
      Forall (uncurry R)
        (same_shape_zip t u Hshape).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
lift_relation R t u ->
Forall (uncurry R) (same_shape_zip t u Hshape)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
lift_relation R t u ->
Forall (uncurry R) (same_shape_zip t u Hshape)
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
Forall (uncurry R) (same_shape_zip t u Hshape)
    unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R) (same_shape_zip t u Hshape)
    unfold same_shape_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R)
  (trav_make t (same_shape_zip_contents t u Hshape))
    rewrite mapReduce_trav_make.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R)
  (same_shape_zip_contents t u Hshape)
    rewrite Monoid_op_Opposite_and.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R)
  (same_shape_zip_contents t u Hshape)
    unfold same_shape_zip_contents.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R)
  (Vector_zip A B (plength t) (plength u)
     (trav_contents t) (trav_contents u)
     (same_shape_implies_plength t u Hshape))
    unfold Vector_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
mapReduce (uncurry R)
  (Vector_zip_eq (trav_contents t)
     (coerce eq_sym
               (same_shape_implies_plength t u Hshape)
      in trav_contents u))
    rewrite <- (traverse_zipped_vector
                 (R := R) (plength t) (trav_contents t)
                 (coerce eq_sym (same_shape_implies_plength t u Hshape)
                   in trav_contents u)).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u Hshape)
   in trav_contents u)
    pose relation2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
t0:= relation2: forall (A B : Type) 
  (R : A -> B -> Prop) 
  (t : T A) (u : T B)
  (Hlen : plength u = plength t),
lift_relation R t u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u Hshape)
   in trav_contents u)
    apply t0.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
H3: lift_relation R t u
t0:= relation2: forall (A B : Type) 
  (R : A -> B -> Prop) 
  (t : T A) (u : T B)
  (Hlen : plength u = plength t),
lift_relation R t u ->
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
lift_relation R t u
    assumption.
  Qed.

  Lemma mapReduce_same_shape_zip `{Monoid M}:
    forall (A B: Type) (f: A * B -> M) (t: T A) (u: T B)
      (Hshape: shape (H := H) t = shape u),
      mapReduce (T := T) f (same_shape_zip t u Hshape) =
        mapReduce (op := Monoid_op_Opposite op) (T := Vector (plength t))
          f (same_shape_zip_contents t u Hshape).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H3: Monoid M
forall (A B : Type) (f : A * B -> M) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
mapReduce f (same_shape_zip t u Hshape) =
mapReduce f (same_shape_zip_contents t u Hshape)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H3: Monoid M
forall (A B : Type) (f : A * B -> M) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
mapReduce f (same_shape_zip t u Hshape) =
mapReduce f (same_shape_zip_contents t u Hshape)
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H3: Monoid M
A, B: Type
f: A * B -> M
t: T A
u: T B
Hshape: shape t = shape u
mapReduce f (same_shape_zip t u Hshape) =
mapReduce f (same_shape_zip_contents t u Hshape)
    unfold same_shape_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H3: Monoid M
A, B: Type
f: A * B -> M
t: T A
u: T B
Hshape: shape t = shape u
mapReduce f
  (trav_make t (same_shape_zip_contents t u Hshape)) =
mapReduce f (same_shape_zip_contents t u Hshape)
    rewrite mapReduce_trav_make.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H3: Monoid M
A, B: Type
f: A * B -> M
t: T A
u: T B
Hshape: shape t = shape u
mapReduce f (same_shape_zip_contents t u Hshape) =
mapReduce f (same_shape_zip_contents t u Hshape)
    reflexivity.
  Qed.

  Lemma relation_to_zipped_iff:
    forall (A B: Type) (R: A -> B -> Prop) (t: T A) (u: T B)
      (Hshape: shape (H :=H) t = shape u),
      lift_relation R t u <->
        (forall C, trav_make (B := C) t ~!~ trav_make u) /\
          Forall (uncurry R)
            (same_shape_zip t u Hshape).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
lift_relation R t u <->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B : Type) (R : A -> B -> Prop) (t : T A)
  (u : T B) (Hshape : shape t = shape u),
lift_relation R t u <->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape)
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
lift_relation R t u <->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape)
    split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
lift_relation R t u ->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape) ->
lift_relation R t u
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
lift_relation R t u ->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape) introv Hrel.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape) split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
forall C : Type, trav_make t ~!~ trav_make u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
Forall (uncurry R) (same_shape_zip t u Hshape)
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
forall C : Type, trav_make t ~!~ trav_make u eapply relation4.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
lift_relation ?R t u
        eassumption.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
Forall (uncurry R) (same_shape_zip t u Hshape) apply relation_to_zipped.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hrel: lift_relation R t u
lift_relation R t u
        assumption.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry R) (same_shape_zip t u Hshape) ->
lift_relation R t u intros [Hmake Hzip].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
lift_relation R t u
      rewrite relation_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\ trav_make t b = u
      assert (Hlen: plength u = plength t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
plength u = plength t
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\ trav_make t b = u
      {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
plength u = plength t apply same_shape_implies_plength.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
shape u = shape t
        symmetry.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
shape t = shape u assumption. }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
exists b : Vector (plength t) B,
  traverse R (trav_contents t) b /\ trav_make t b = u
      exists (coerce Hlen in trav_contents u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) /\
trav_make t (coerce Hlen in trav_contents u) = u
      split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t (coerce Hlen in trav_contents u) = u
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u) unfold same_shape_zip in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R)
  (trav_make t
     (same_shape_zip_contents t u Hshape))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        unfold same_shape_zip_contents in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R)
  (trav_make t
     (Vector_zip A B 
        (plength t) 
        (plength u) 
        (trav_contents t) 
        (trav_contents u)
        (same_shape_implies_plength t u Hshape)))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        unfold Vector_zip in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R)
  (trav_make t
     (Vector_zip_eq 
        (trav_contents t)
        (coerce 
         eq_sym
           (same_shape_implies_plength t u
             Hshape) in 
         trav_contents u)))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        unfold Forall in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: mapReduce (uncurry R)
  (trav_make t
     (Vector_zip_eq 
        (trav_contents t)
        (coerce 
         eq_sym
           (same_shape_implies_plength t u
             Hshape) in 
         trav_contents u)))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        rewrite mapReduce_trav_make in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: mapReduce (uncurry R)
  (Vector_zip_eq 
     (trav_contents t)
     (coerce eq_sym
             (same_shape_implies_plength t u
             Hshape) in 
      trav_contents u))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        rewrite Monoid_op_Opposite_and in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: mapReduce (uncurry R)
  (Vector_zip_eq 
     (trav_contents t)
     (coerce eq_sym
             (same_shape_implies_plength t u
             Hshape) in 
      trav_contents u))
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        rewrite <- (traverse_zipped_vector
                     (R := R) (plength t) (trav_contents t)
                     (coerce eq_sym (same_shape_implies_plength t u Hshape)
                       in trav_contents u)) in Hzip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
        enough (Hcoerce: (coerce eq_sym (same_shape_implies_plength t u Hshape)
                   in trav_contents u) =
                  coerce Hlen in trav_contents u).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
Hcoerce: coerce eq_sym
         (same_shape_implies_plength t u
            Hshape) in 
trav_contents u =
coerce Hlen in trav_contents u
traverse R (trav_contents t)
  (coerce Hlen in trav_contents u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
coerce eq_sym (same_shape_implies_plength t u Hshape)
in trav_contents u = 
coerce Hlen in trav_contents u
        rewrite <- Hcoerce.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
Hcoerce: coerce eq_sym
         (same_shape_implies_plength t u
            Hshape) in 
trav_contents u =
coerce Hlen in trav_contents u
traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u Hshape)
   in trav_contents u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
coerce eq_sym (same_shape_implies_plength t u Hshape)
in trav_contents u = 
coerce Hlen in trav_contents u
        assumption.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
coerce eq_sym (same_shape_implies_plength t u Hshape)
in trav_contents u = coerce Hlen in trav_contents u
        apply Vector_sim_eq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: traverse R (trav_contents t)
  (coerce eq_sym
            (same_shape_implies_plength t u
             Hshape) in 
   trav_contents u)
Hlen: plength u = plength t
coerce eq_sym (same_shape_implies_plength t u Hshape)
in trav_contents u ~~ coerce Hlen in trav_contents u
        vector_sim.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t (coerce Hlen in trav_contents u) = u change u with (id u) at 3.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t (coerce Hlen in trav_contents u) = id u
        rewrite id_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t (coerce Hlen in trav_contents u) =
trav_make u (trav_contents u)
        apply Vector_fun_sim_eq.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t ~!~ trav_make u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
coerce Hlen in trav_contents u ~~ trav_contents u
        *
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
trav_make t ~!~ trav_make u apply Hmake.
        *
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B: Type
R: A -> B -> Prop
t: T A
u: T B
Hshape: shape t = shape u
Hmake: forall C : Type, trav_make t ~!~ trav_make u
Hzip: Forall (uncurry R) (same_shape_zip t u Hshape)
Hlen: plength u = plength t
coerce Hlen in trav_contents u ~~ trav_contents u vector_sim.
  Qed.

  Lemma relation_natural1:
    forall (A B1 B2: Type) (R: B1 -> B2 -> Prop) (t: T A) (f: A -> B1),
      lift_relation R (map f t) = lift_relation (R ∘ map f) t.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B1 B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T A) (f : A -> B1),
lift_relation R (map f t) =
lift_relation (R ∘ map f) t
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B1 B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T A) (f : A -> B1),
lift_relation R (map f t) =
lift_relation (R ∘ map f) t
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
lift_relation R (map f t) =
lift_relation (R ∘ map f) t
    unfold lift_relation.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
traverse R (map f t) = traverse (R ∘ map f) t
    compose near t on left.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
(traverse R ∘ map f) t = traverse (R ∘ map f) t
    rewrite (traverse_map (G2 := subset) R f).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
traverse (R ∘ f) t = traverse (R ∘ map f) t
    reflexivity.
  Qed.

  Lemma relation_natural2_lemma:
    forall (B1 A B2: Type) (R: B1 -> B2 -> Prop) (t: T B1) (u: T A) (f: A -> B2)
      (Hshape: shape (H := H) t = shape (map f u))
      (Hshape': shape (H := H)  t = shape u),
      Forall (uncurry R) (same_shape_zip t (map f u) Hshape) =
        Forall (uncurry (precompose f ∘ R)) (same_shape_zip t u Hshape').
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2)
  (Hshape : shape t = shape (map f u))
  (Hshape' : shape t = shape u),
Forall (uncurry R) (same_shape_zip t (map f u) Hshape) =
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape')
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2)
  (Hshape : shape t = shape (map f u))
  (Hshape' : shape t = shape u),
Forall (uncurry R) (same_shape_zip t (map f u) Hshape) =
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape')
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
Forall (uncurry R) (same_shape_zip t (map f u) Hshape) =
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape')
    unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
mapReduce (uncurry R)
  (same_shape_zip t (map f u) Hshape) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape')
    rewrite mapReduce_same_shape_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
mapReduce (uncurry R)
  (same_shape_zip_contents t (map f u) Hshape) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape')
    rewrite mapReduce_same_shape_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
mapReduce (uncurry R)
  (same_shape_zip_contents t (map f u) Hshape) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip_contents t u Hshape')
    rewrite natural_snd_same_shape_zip_contents_rev.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
mapReduce (uncurry R)
  (map (map_snd f)
     (same_shape_zip_contents t u
        (same_shape_map_rev_r t u f Hshape))) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip_contents t u Hshape')
    compose near (same_shape_zip_contents t u (same_shape_map_rev_r t u f Hshape)).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
(mapReduce (uncurry R) ∘ map (map_snd f))
  (same_shape_zip_contents t u
     (same_shape_map_rev_r t u f Hshape)) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip_contents t u Hshape')
    rewrite (mapReduce_map).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
mapReduce (uncurry R ∘ map_snd f)
  (same_shape_zip_contents t u
     (same_shape_map_rev_r t u f Hshape)) =
mapReduce (uncurry (precompose f ∘ R))
  (same_shape_zip_contents t u Hshape')
    fequal.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
uncurry R ∘ map_snd f = uncurry (precompose f ∘ R)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
same_shape_zip_contents t u
  (same_shape_map_rev_r t u f Hshape) =
same_shape_zip_contents t u Hshape'
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
uncurry R ∘ map_snd f = uncurry (precompose f ∘ R) ext [x y].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
x: B1
y: A
(uncurry R ∘ map_snd f) (x, y) =
uncurry (precompose f ∘ R) (x, y) reflexivity.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape (map f u)
Hshape': shape t = shape u
same_shape_zip_contents t u
  (same_shape_map_rev_r t u f Hshape) =
same_shape_zip_contents t u Hshape' apply same_shape_zip_contents_proof_irrelevance.
  Qed.

  Lemma relation_natural2_core:
    forall (B1 A B2: Type) (R: B1 -> B2 -> Prop) (t: T B1) (u: T A) (f: A -> B2),
      shape t = shape u ->
      lift_relation R t (map f u) = lift_relation (precompose f ∘ R) t u.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2),
shape t = shape u ->
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2),
shape t = shape u ->
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    introv Hshape.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    assert (Hshape': shape t = shape (map f u)).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
shape t = shape (map f u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
shape t = shape (map f u) rewrite shape_map.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
shape t = shape u assumption. }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    apply propositional_extensionality.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
lift_relation R t (map f u) <->
lift_relation (precompose f ∘ R) t u
    rewrite (relation_to_zipped_iff _ _ R t (map f u) Hshape').
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry R)
  (same_shape_zip t (map f u) Hshape') <->
lift_relation (precompose f ∘ R) t u
    rewrite (relation_to_zipped_iff _ _ (precompose f ∘ R) t u Hshape).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry R)
  (same_shape_zip t (map f u) Hshape') <->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
    erewrite relation_natural2_lemma.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape') <->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
    split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape') ->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) ->
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape') ->
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) intros [X1 X2].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
forall C : Type, trav_make t ~!~ trav_make u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
forall C : Type, trav_make t ~!~ trav_make u intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
C: Type
trav_make t ~!~ trav_make u
        apply trav_same_shape.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
C: Type
shape t = shape u
        assumption.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type,
trav_make t ~!~ trav_make (map f u)
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u ?Hshape')
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) eassumption.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
(forall C : Type, trav_make t ~!~ trav_make u) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) ->
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) intros [X1 X2].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
(forall C : Type, trav_make t ~!~ trav_make (map f u)) /\
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
forall C : Type, trav_make t ~!~ trav_make (map f u)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
forall C : Type, trav_make t ~!~ trav_make (map f u) apply trav_same_shape.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
shape t = shape (map f u)
        assumption.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
Hshape: shape t = shape u
Hshape': shape t = shape (map f u)
X1: forall C : Type, trav_make t ~!~ trav_make u
X2: Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape)
Forall (uncurry (precompose f ∘ R))
  (same_shape_zip t u Hshape) assumption.
  Qed.

  Lemma relation_natural2:
    forall (B1 A B2: Type) (R: B1 -> B2 -> Prop) (t: T B1) (u: T A) (f: A -> B2),
      lift_relation R t (map f u) = lift_relation (precompose f ∘ R) t u.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2),
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (B1 A B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T B1) (u : T A) (f : A -> B2),
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation R t (map f u) =
lift_relation (precompose f ∘ R) t u
    apply propositional_extensionality.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation R t (map f u) <->
lift_relation (precompose f ∘ R) t u
    split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation R t (map f u) ->
lift_relation (precompose f ∘ R) t u
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation (precompose f ∘ R) t u ->
lift_relation R t (map f u)
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation R t (map f u) ->
lift_relation (precompose f ∘ R) t u introv hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: lift_relation R t (map f u)
lift_relation (precompose f ∘ R) t u
      rewrite <- relation_natural2_core; try assumption.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: lift_relation R t (map f u)
shape t = shape u
      apply relation_implies_shape in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: shape t = shape (map f u)
shape t = shape u
      rewrite shape_map in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: shape t = shape u
shape t = shape u
      assumption.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
lift_relation (precompose f ∘ R) t u ->
lift_relation R t (map f u) introv hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: lift_relation (precompose f ∘ R) t u
lift_relation R t (map f u)
      rewrite relation_natural2_core; try assumption.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: lift_relation (precompose f ∘ R) t u
shape t = shape u
      apply relation_implies_shape in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
B1, A, B2: Type
R: B1 -> B2 -> Prop
t: T B1
u: T A
f: A -> B2
hyp: shape t = shape u
shape t = shape u
      assumption.
  Qed.

  (* TODO This can actually be strengthed into an IFF *)
  Lemma relation_respectful:
    forall (A B1 B2: Type) (R: B1 -> B2 -> Prop) (t: T A) (f: A -> B1) (g: A -> B2),
    (forall (a: A), a ∈ t -> R (f a) (g a)) -> lift_relation R (map f t) (map g t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B1 B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T A) (f : A -> B1) (g : A -> B2),
(forall a : A, a ∈ t -> R (f a) (g a)) ->
lift_relation R (map f t) (map g t)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
forall (A B1 B2 : Type) (R : B1 -> B2 -> Prop)
  (t : T A) (f : A -> B1) (g : A -> B2),
(forall a : A, a ∈ t -> R (f a) (g a)) ->
lift_relation R (map f t) (map g t)
    introv hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
lift_relation R (map f t) (map g t)
    rewrite relation_natural1.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
lift_relation (R ∘ map f) t (map g t)
    rewrite relation_natural2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
lift_relation (precompose g ∘ (R ∘ map f)) t t
    unfold lift_relation.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
traverse (precompose g ∘ (R ∘ map f)) t t
    rewrite traverse_through_runBatch.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
(runBatch (precompose g ∘ (R ∘ map f)) ∘ toBatch) t t
    unfold compose.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, a ∈ t -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) t
    unfold element_of in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, tosubset t a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) t
    rewrite tosubset_to_mapReduce in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, mapReduce ret t a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) t
    change t with (id t) at 2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, mapReduce ret t a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) (id t)
    rewrite id_through_runBatch.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, mapReduce ret t a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) ((runBatch id ∘ toBatch) t)
    unfold compose.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A, mapReduce ret t a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) (runBatch id (toBatch t))
    rewrite (mapReduce_through_toBatch A A) in hyp.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (toBatch t) (runBatch id (toBatch t))
    (* induction (@toBatch T ToBatch_inst A A t). *) (* Generates a weird hypothesis *)
    apply (Batch_ind A A
      (fun (C: Type) (b: Batch A A C) =>
           (forall a: A, mapReduce (T := BATCH1 A C) (ret (T := subset)) b a -> R (f a) (g a)) ->
           runBatch (G := subset) (fun a: A => precompose g (R (map f a))) b (runBatch id b))).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall (C : Type) (c : C),
(forall a : A,
 mapReduce ret (Done c) a -> R (f a) (g a)) ->
runBatch (fun a : A => precompose g (R (map f a)))
  (Done c) (runBatch id (Done c))
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall (C : Type) (b : Batch A A (A -> C)),
((forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
 runBatch (fun a : A => precompose g (R (map f a))) b
   (runBatch id b)) ->
forall a : A,
(forall a0 : A,
 mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)) ->
runBatch (fun a0 : A => precompose g (R (map f a0)))
  (b ⧆ a) (runBatch id (b ⧆ a))
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall (C : Type) (c : C),
(forall a : A,
 mapReduce ret (Done c) a -> R (f a) (g a)) ->
runBatch (fun a : A => precompose g (R (map f a)))
  (Done c) (runBatch id (Done c)) intros C c hyp'.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
c: C
hyp': forall a : A,
mapReduce ret (Done c) a -> R (f a) (g a)
runBatch (fun a : A => precompose g (R (map f a)))
  (Done c) (runBatch id (Done c))
      reflexivity.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall (C : Type) (b : Batch A A (A -> C)),
((forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
 runBatch (fun a : A => precompose g (R (map f a))) b
   (runBatch id b)) ->
forall a : A,
(forall a0 : A,
 mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)) ->
runBatch (fun a0 : A => precompose g (R (map f a0)))
  (b ⧆ a) (runBatch id (b ⧆ a)) introv IH.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
forall a : A,
(forall a0 : A,
 mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)) ->
runBatch (fun a0 : A => precompose g (R (map f a0)))
  (b ⧆ a) (runBatch id (b ⧆ a))
      introv hyp'.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch (fun a : A => precompose g (R (map f a)))
  (b ⧆ a) (runBatch id (b ⧆ a))
      rewrite runBatch_rw2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
(runBatch (fun a : A => precompose g (R (map f a))) b <⋆>
 precompose g (R (map f a))) (runBatch id (b ⧆ a))
      rewrite runBatch_rw2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
(runBatch (fun a : A => precompose g (R (map f a))) b <⋆>
 precompose g (R (map f a))) (runBatch id b <⋆> id a)
      rewrite subset_ap_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
exists (f0 : A -> C) (a0 : A),
  precompose g (R (map f a)) a0 /\
  runBatch (fun a : A => precompose g (R (map f a))) b
    f0 /\ f0 a0 = runBatch id b <⋆> id a
      unfold ap.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
exists (f0 : A -> C) (a0 : A),
  precompose g (R (map f a)) a0 /\
  runBatch (fun a : A => precompose g (R (map f a))) b
    f0 /\
  f0 a0 =
  map (fun '(f, a) => f a) (runBatch id b ⊗ id a)
      unfold_ops @Map_I.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
exists (f0 : A -> C) (a0 : A),
  precompose g (R (f a)) a0 /\
  runBatch (fun a : A => precompose g (R (f a))) b f0 /\
  f0 a0 = (let '(f, a) := runBatch id b ⊗ id a in f a)
      unfold_ops @Mult_I.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
exists (f0 : A -> C) (a0 : A),
  precompose g (R (f a)) a0 /\
  runBatch (fun a : A => precompose g (R (f a))) b f0 /\
  f0 a0 = runBatch id b (id a)
      exists (runBatch id b) a.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
precompose g (R (f a)) a /\
runBatch (fun a : A => precompose g (R (f a))) b
  (runBatch id b) /\
runBatch id b a = runBatch id b (id a)
      splits.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
precompose g (R (f a)) a
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch (fun a : A => precompose g (R (f a))) b
  (runBatch id b)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch id b a = runBatch id b (id a)
      {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
precompose g (R (f a)) a unfold precompose, compose.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
R (f a) (g a)
        unfold_ops @Map_I.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
R (f a) (g a)
        apply hyp'.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
mapReduce ret (b ⧆ a) a
        now right. }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch (fun a : A => precompose g (R (f a))) b
  (runBatch id b)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch id b a = runBatch id b (id a)
      {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch (fun a : A => precompose g (R (f a))) b
  (runBatch id b) apply IH.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
forall a : A, mapReduce ret b a -> R (f a) (g a)
        intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
a0: A
H3: mapReduce ret b a0
R (f a0) (g a0)
        apply hyp'.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
a0: A
H3: mapReduce ret b a0
mapReduce ret (b ⧆ a) a0
        rewrite mapReduce_Batch_rw2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
a0: A
H3: mapReduce ret b a0
(mapReduce ret b ● ret a) a0
        now left.
      }
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch id b a = runBatch id b (id a)
      {
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
C: Type
b: Batch A A (A -> C)
IH: (forall a : A, mapReduce ret b a -> R (f a) (g a)) ->
runBatch
  (fun a : A => precompose g (R (map f a))) b
  (runBatch id b)
a: A
hyp': forall a0 : A,
mapReduce ret (b ⧆ a) a0 -> R (f a0) (g a0)
runBatch id b a = runBatch id b (id a) reflexivity. }
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
H2: ToSubset T
Compat_ToSubset_Traverse0: Compat_ToSubset_Traverse T
A, B1, B2: Type
R: B1 -> B2 -> Prop
t: T A
f: A -> B1
g: A -> B2
hyp: forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a)
forall a : A,
mapReduce ret (toBatch t) a -> R (f a) (g a) assumption.
  Qed.

End lifting_relations.


(** * Properties of Relations *)
(**********************************************************************)
Section relprop.


End relprop.

(** * Diagonal *)
(**********************************************************************)
Section relprop.

  Context
    `{Classes.Categorical.TraversableFunctor.TraversableFunctor T}.

  Import CategoricalToKleisli.TraversableFunctor.DerivedOperations.
  Import CategoricalToKleisli.TraversableFunctor.DerivedInstances.
  Import KleisliToCoalgebraic.TraversableFunctor.DerivedOperations.
  Import KleisliToCoalgebraic.TraversableFunctor.DerivedInstances.

  Lemma relation_diagonal1:
    forall (A: Type) (R: A -> A -> Prop) (t: T A),
      Forall (fun (a: A) => R a a) t -> lift_relation R t t.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
Forall (fun a : A => R a a) t -> lift_relation R t t
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
Forall (fun a : A => R a a) t -> lift_relation R t t
    introv HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: Forall (fun a : A => R a a) t
lift_relation R t t
    unfold Forall in HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: mapReduce (fun a : A => R a a) t
lift_relation R t t
    rewrite (mapReduce_to_traverse2 A) in HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: traverse (fun a : A => R a a) t
lift_relation R t t
    unfold lift_relation.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: traverse (fun a : A => R a a) t
traverse R t t
    rewrite traverse_through_runBatch in HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
traverse R t t
    rewrite traverse_through_runBatch.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
(runBatch R ∘ toBatch) t t
    unfold compose.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
runBatch R (toBatch t) t
    change t with (id t) at 2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
runBatch R (toBatch t) (id t)
    rewrite (id_through_runBatch).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
runBatch R (toBatch t) ((runBatch id ∘ toBatch) t)
    unfold compose at 1.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: (runBatch (fun a : A => R a a) ∘ toBatch) t
runBatch R (toBatch t) (runBatch id (toBatch t))
    unfold compose at 1 in HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
HF: runBatch (fun a : A => R a a) (toBatch t)
runBatch R (toBatch t) (runBatch id (toBatch t))
    generalize dependent HF.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
runBatch (fun a : A => R a a) (toBatch t) ->
runBatch R (toBatch t) (runBatch id (toBatch t))

    apply (Batch_ind A A
             (fun C (b: Batch A A C) =>
                runBatch (G := const Prop) (fun a: A => R a a) b ->
                runBatch (G := subset) R b (runBatch id b))).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
forall (C : Type) (c : C),
runBatch (fun a : A => R a a) (Done c) ->
runBatch R (Done c) (runBatch id (Done c))
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
forall (C : Type) (b : Batch A A (A -> C)),
(runBatch (fun a : A => R a a) b ->
 runBatch R b (runBatch id b)) ->
forall a : A,
runBatch (fun a0 : A => R a0 a0) (b ⧆ a) ->
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
forall (C : Type) (c : C),
runBatch (fun a : A => R a a) (Done c) ->
runBatch R (Done c) (runBatch id (Done c)) cbv.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
forall (C : Type) (c : C), True -> c = c tauto.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
forall (C : Type) (b : Batch A A (A -> C)),
(runBatch (fun a : A => R a a) b ->
 runBatch R b (runBatch id b)) ->
forall a : A,
runBatch (fun a0 : A => R a0 a0) (b ⧆ a) ->
runBatch R (b ⧆ a) (runBatch id (b ⧆ a)) introv X1 X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: runBatch (fun a : A => R a a) (b ⧆ a)
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      rewrite runBatch_rw2 in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: runBatch (fun a : A => R a a) b <⋆> R a a
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold ap in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: map (fun '(f, a) => f a)
  (runBatch (fun a : A => R a a) b ⊗ R a a)
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold map in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: Map_const ((A -> C) * A) C (fun '(f, a) => f a)
  (runBatch (fun a : A => R a a) b ⊗ R a a)
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold Map_const in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: runBatch (fun a : A => R a a) b ⊗ R a a
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold mult in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: Mult_const (A -> C) A
  (runBatch (fun a : A => R a a) b, R a a)
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold Mult_const in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: runBatch (fun a : A => R a a) b ● R a a
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold monoid_op in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: Monoid_op_and (runBatch (fun a : A => R a a) b)
  (R a a)
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      unfold Monoid_op_and in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
X2: runBatch (fun a : A => R a a) b /\ R a a
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      destruct X2 as [Y1 Y2].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
runBatch R (b ⧆ a) (runBatch id (b ⧆ a))
      rewrite runBatch_rw2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
(runBatch R b <⋆> R a) (runBatch id (b ⧆ a))
      rewrite runBatch_rw2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
(runBatch R b <⋆> R a) (runBatch id b <⋆> id a)
      rewrite subset_ap_spec.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
exists (f : A -> C) (a0 : A),
  R a a0 /\
  runBatch R b f /\ f a0 = runBatch id b <⋆> id a
      exists (runBatch id b).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
exists a0 : A,
  R a a0 /\
  runBatch R b (runBatch id b) /\
  runBatch id b a0 = runBatch id b <⋆> id a
      exists a.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
C: Type
b: Batch A A (A -> C)
X1: runBatch (fun a : A => R a a) b ->
runBatch R b (runBatch id b)
a: A
Y1: runBatch (fun a : A => R a a) b
Y2: R a a
R a a /\
runBatch R b (runBatch id b) /\
runBatch id b a = runBatch id b <⋆> id a
      split; auto.
  Qed.

  Lemma Forall_vector:
    forall (A: Type) (R: A -> Prop) (t: T A),
      Forall R t = Forall R (trav_contents t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> Prop) (t : T A),
Forall R t = Forall R (trav_contents t)
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> Prop) (t : T A),
Forall R t = Forall R (trav_contents t)
    unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> Prop) (t : T A),
mapReduce R t = mapReduce R (trav_contents t)
    intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
mapReduce R t = mapReduce R (trav_contents t)
    rewrite mapReduce_to_traverse1.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
traverse R t = mapReduce R (trav_contents t)
    rewrite traverse_repr.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
map (trav_make t)
  (forwards
     (traverse (mkBackwards ∘ R) (trav_contents t))) =
mapReduce R (trav_contents t)
    induction (trav_contents t) using Vector_induction.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
map (trav_make t)
  (forwards (traverse (mkBackwards ∘ R) vnil)) =
mapReduce R vnil
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards (traverse (mkBackwards ∘ R) (vcons m a v))) =
mapReduce R (vcons m a v)
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
map (trav_make t)
  (forwards (traverse (mkBackwards ∘ R) vnil)) =
mapReduce R vnil cbn.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
pure
  (exist (fun l : list False => length l = 0) nil
     eq_refl) =
pure
  (exist (fun l : list False => length l = 0) nil
     eq_refl)
      reflexivity.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards (traverse (mkBackwards ∘ R) (vcons m a v))) =
mapReduce R (vcons m a v) rewrite traverse_Vector_vcons.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards
     (pure (vcons m) <⋆> (mkBackwards ∘ R) a <⋆>
      traverse (mkBackwards ∘ R) v)) =
mapReduce R (vcons m a v)
      rewrite mapReduce_to_traverse1.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards
     (pure (vcons m) <⋆> (mkBackwards ∘ R) a <⋆>
      traverse (mkBackwards ∘ R) v)) =
traverse R (vcons m a v)
      rewrite traverse_Vector_vcons.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards
     (pure (vcons m) <⋆> (mkBackwards ∘ R) a <⋆>
      traverse (mkBackwards ∘ R) v)) =
pure (vcons m) <⋆> R a <⋆> traverse R v
      rewrite <- mapReduce_to_traverse1.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
map (trav_make t)
  (forwards
     (pure (vcons m) <⋆> (mkBackwards ∘ R) a <⋆>
      traverse (mkBackwards ∘ R) v)) =
pure (vcons m) <⋆> R a <⋆> mapReduce R v
      cbn.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
forwards (traverse (mkBackwards ∘ R) v)
● (R a ● pure (vcons m)) =
(pure (vcons m) ● R a) ● mapReduce R v
      rewrite <- IHv.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
forwards (traverse (mkBackwards ∘ R) v)
● (R a ● pure (vcons m)) =
(pure (vcons m) ● R a)
● map (trav_make t)
    (forwards (traverse (mkBackwards ∘ R) v))
      cbn.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
forwards (traverse (mkBackwards ∘ R) v)
● (R a ● pure (vcons m)) =
(pure (vcons m) ● R a)
● map (trav_make t)
    (forwards (traverse (mkBackwards ∘ R) v))
      unfold transparent tcs.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
(forwards
   (traverse_Vector m (Backwards (const Prop))
      (mkBackwards ∘ R) v) /\ R a /\ Ƶ) =
((Ƶ /\ R a) /\
 (let (forwards) :=
    traverse_Vector m (Backwards (const Prop))
      (mkBackwards ∘ R) v in
  forwards))
      unfold transparent tcs.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
(forwards
   (traverse_Vector m (Backwards (const Prop))
      (mkBackwards ∘ R) v) /\ R a /\ True) =
((True /\ R a) /\
 (let (forwards) :=
    traverse_Vector m (Backwards (const Prop))
      (mkBackwards ∘ R) v in
  forwards))
      propext.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True ->
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards)
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards) ->
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True ->
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards) intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
H2: forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards)
        preprocess.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
H2: forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v)
H3: R a
H4: True
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards)
        split; auto.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
(True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards) ->
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True intros.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
H2: (True /\ R a) /\
(let (forwards) :=
   traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v in
 forwards)
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True
        preprocess.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> Prop
t: T A
a: A
m: nat
v: Vector m A
IHv: map (trav_make t) (forwards (traverse (mkBackwards ∘ R) v)) = mapReduce R v
H2: True
H4: R a
H3: let (forwards) :=
  traverse_Vector m (Backwards (const Prop))
    (mkBackwards ∘ R) v in
forwards
forwards
  (traverse_Vector m (Backwards (const Prop))
     (mkBackwards ∘ R) v) /\ R a /\ True
        split; auto.
  Qed.

  Lemma relation_diagonal2:
    forall (A: Type) (R: A -> A -> Prop) (t: T A),
      lift_relation R t t -> Forall (fun (a: A) => R a a) t.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
lift_relation R t t -> Forall (fun a : A => R a a) t
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
lift_relation R t t -> Forall (fun a : A => R a a) t
    introv.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
lift_relation R t t -> Forall (fun a : A => R a a) t
    rewrite (relation_to_zipped_iff _ _ R t t (eq_refl)).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
(forall C : Type, trav_make t ~!~ trav_make t) /\
Forall (uncurry R) (same_shape_zip t t eq_refl) ->
Forall (fun a : A => R a a) t
    intros [X1 X2].
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: Forall (uncurry R) (same_shape_zip t t eq_refl)
Forall (fun a : A => R a a) t
    generalize dependent X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
Forall (uncurry R) (same_shape_zip t t eq_refl) ->
Forall (fun a : A => R a a) t
    unfold same_shape_zip.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
Forall (uncurry R)
  (trav_make t (same_shape_zip_contents t t eq_refl)) ->
Forall (fun a : A => R a a) t
    unfold same_shape_zip_contents.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
Forall (uncurry R)
  (trav_make t
     (Vector_zip A A (plength t) (plength t)
        (trav_contents t) (trav_contents t)
        (same_shape_implies_plength t t eq_refl))) ->
Forall (fun a : A => R a a) t
    rewrite Vector_zip_proof_irrelevance2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
Forall (uncurry R)
  (trav_make t
     (Vector_zip_eq (trav_contents t)
        (trav_contents t))) ->
Forall (fun a : A => R a a) t
    rewrite Vector_zip_diagonal.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
Forall (uncurry R)
  (trav_make t
     (map (fun a : A => (a, a)) (trav_contents t))) ->
Forall (fun a : A => R a a) t
    unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
mapReduce (uncurry R)
  (trav_make t
     (map (fun a : A => (a, a)) (trav_contents t))) ->
mapReduce (fun a : A => R a a) t
    rewrite mapReduce_trav_make.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
mapReduce (uncurry R)
  (map (fun a : A => (a, a)) (trav_contents t)) ->
mapReduce (fun a : A => R a a) t
    compose near (trav_contents t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
(mapReduce (uncurry R) ∘ map (fun a : A => (a, a)))
  (trav_contents t) ->
mapReduce (fun a : A => R a a) t
    rewrite mapReduce_map.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
mapReduce (uncurry R ∘ (fun a : A => (a, a)))
  (trav_contents t) ->
mapReduce (fun a : A => R a a) t
    unfold compose.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
mapReduce (fun a : A => uncurry R (a, a))
  (trav_contents t) ->
mapReduce (fun a : A => R a a) t
    intro.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => uncurry R (a, a))
  (trav_contents t)
mapReduce (fun a : A => R a a) t
    change (Forall (fun a => R a a) t).
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => uncurry R (a, a))
  (trav_contents t)
Forall (fun a : A => R a a) t
    rewrite Forall_vector.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => uncurry R (a, a))
  (trav_contents t)
Forall (fun a : A => R a a) (trav_contents t)
    unfold uncurry in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => R a a) (trav_contents t)
Forall (fun a : A => R a a) (trav_contents t)
    induction (trav_contents t) using Vector_induction.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => R a a) vnil
Forall (fun a : A => R a a) vnil
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: mapReduce (fun a : A => R a a) (vcons m a v)
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
Forall (fun a : A => R a a) (vcons m a v)
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => R a a) vnil
Forall (fun a : A => R a a) vnil unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => R a a) vnil
mapReduce (fun a : A => R a a) vnil
      rewrite mapReduce_Vector_vnil.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
X2: mapReduce (fun a : A => R a a) vnil
Ƶ
      easy.
    -
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: mapReduce (fun a : A => R a a) (vcons m a v)
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
Forall (fun a : A => R a a) (vcons m a v) unfold Forall.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: mapReduce (fun a : A => R a a) (vcons m a v)
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
mapReduce (fun a : A => R a a) (vcons m a v)
      rewrite mapReduce_Vector_vcons.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: mapReduce (fun a : A => R a a) (vcons m a v)
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
R a a ● mapReduce (fun a : A => R a a) v
      rewrite mapReduce_Vector_vcons in X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
R a a ● mapReduce (fun a : A => R a a) v
      inversion X2.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
R a a ● mapReduce (fun a : A => R a a) v
      split.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
R a a
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
mapReduce (fun a : A => R a a) v
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
R a a assumption.
      +
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
mapReduce (fun a : A => R a a) v apply IHv.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
X1: forall C : Type, trav_make t ~!~ trav_make t
a: A
m: nat
v: Vector m A
X2: R a a ● mapReduce (fun a : A => R a a) v
IHv: mapReduce (fun a : A => R a a) v -> Forall (fun a : A => R a a) v
H2: mapReduce (fun a : A => R a a) v
H3: R a a
mapReduce (fun a : A => R a a) v assumption.
  Qed.

  Lemma relation_diagonal_iff:
    forall (A: Type) (R: A -> A -> Prop) (t: T A),
      lift_relation R t t <-> Forall (fun (a: A) => R a a) t.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
lift_relation R t t <-> Forall (fun a : A => R a a) t
  Proof.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
forall (A : Type) (R : A -> A -> Prop) (t : T A),
lift_relation R t t <-> Forall (fun a : A => R a a) t
    introv; split; intro.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
H2: lift_relation R t t
Forall (fun a : A => R a a) t
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
H2: Forall (fun a : A => R a a) t
lift_relation R t t
    apply relation_diagonal2; auto.
T: Type -> Type
H: Map T
H0: TraversableFunctor.ApplicativeDist T
H1: Categorical.TraversableFunctor.TraversableFunctor
  T
A: Type
R: A -> A -> Prop
t: T A
H2: Forall (fun a : A => R a a) t
lift_relation R t t
    apply relation_diagonal1; auto.
  Qed.

End relprop.