From Tealeaves Require Export
  Classes.Functor
  Classes.Kleisli.ContainerMonad
  Classes.Kleisli.Monad.

#[local] Generalizable Variables U T A B.

Import ContainerFunctor.Notations.

(** * Derived Properties of <<ContainerMonad>> *)
(**********************************************************************)
Section corollaries.

  Context
    `{ContainerMonad T}
    `{Map_inst: Map T}
    `{! Compat_Map_Bind T T}.

  (** ** <<ret>> is Injective *)
  (********************************************************************)
  Lemma ret_injective: forall (A: Type) (a a': A),
      ret a = ret a' -> a = a'.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (a a' : A), ret a = ret a' -> a = a'
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (a a' : A), ret a = ret a' -> a = a'
    introv hyp.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
a = a'
    cut (tosubset (ret a) = tosubset (ret a')).
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a') -> a = a'
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a')
    compose near a.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
(tosubset ∘ ret) a = tosubset (ret a') -> a = a'
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a')
    compose near a'.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
(tosubset ∘ ret) a = (tosubset ∘ ret) a' -> a = a'
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a')
    rewrite (kmon_hom_ret (ϕ := @tosubset T _)).
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
ret a = ret a' -> a = a'
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a')
    now apply set_ret_injective.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a, a': A
hyp: ret a = ret a'
tosubset (ret a) = tosubset (ret a')
    now rewrite hyp.
  Qed.

  (** ** Specification of <<a ∈ ret ->> *)
  (********************************************************************)
  Theorem in_ret_iff:
    forall (A: Type) (a1 a2: A), a1 ∈ ret a2 <-> a1 = a2.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (a1 a2 : A), a1 ∈ ret a2 <-> a1 = a2
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (a1 a2 : A), a1 ∈ ret a2 <-> a1 = a2
    intros.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a1, a2: A
a1 ∈ ret a2 <-> a1 = a2
    compose near a2 on left.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a1, a2: A
(element_of a1 ∘ ret) a2 <-> a1 = a2
    rewrite element_of_tosubset.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a1, a2: A
(evalAt a1 ∘ tosubset ∘ ret) a2 <-> a1 = a2
    reassociate -> on left.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a1, a2: A
(evalAt a1 ∘ (tosubset ∘ ret)) a2 <-> a1 = a2
    rewrite (kmon_hom_ret (ϕ := @tosubset T _)).
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
a1, a2: A
(evalAt a1 ∘ ret) a2 <-> a1 = a2
    easy.
  Qed.

  (** ** Specification of <<b ∈ bind f t>> *)
  (********************************************************************)
  Theorem in_bind_iff:
    forall `(f: A -> T B) (t: T A) (b: B),
      b ∈ bind f t <-> exists a, a ∈ t /\ b ∈ f a.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> T B) (t : T A) (b : B),
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a)
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f : A -> T B) (t : T A) (b : B),
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a)
    intros.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> T B
t: T A
b: B
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a) compose near t on left.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> T B
t: T A
b: B
(element_of b ∘ bind f) t <->
(exists a : A, a ∈ t /\ b ∈ f a)
    rewrite element_of_tosubset.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> T B
t: T A
b: B
(evalAt b ∘ tosubset ∘ bind f) t <->
(exists a : A, a ∈ t /\ (evalAt b ∘ tosubset) (f a))
    reassociate -> on left.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> T B
t: T A
b: B
(evalAt b ∘ (tosubset ∘ bind f)) t <->
(exists a : A, a ∈ t /\ (evalAt b ∘ tosubset) (f a))
    rewrite (kmon_hom_bind (ϕ := @tosubset T _)).
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f: A -> T B
t: T A
b: B
(evalAt b ∘ (bind (tosubset ∘ f) ∘ tosubset)) t <->
(exists a : A, a ∈ t /\ (evalAt b ∘ tosubset) (f a))
    reflexivity.
  Qed.

  (** ** Respectfulness Properties for <<bind>> *)
  (********************************************************************)
  (** This is just a more convenient name for consistency *)
  Corollary bind_respectful: forall (A B: Type) (t: T A) (f g: A -> T B),
      (forall a, a ∈ t -> f a = g a) -> bind f t = bind g t.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (t : T A) (f g : A -> T B),
(forall a : A, a ∈ t -> f a = g a) ->
bind f t = bind g t
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (t : T A) (f g : A -> T B),
(forall a : A, a ∈ t -> f a = g a) ->
bind f t = bind g t
    exact contm_pointwise.
  Qed.

  Corollary bind_respectful_map:
    forall `(f1: A -> T B) `(f2: A -> B) (t: T A),
      (forall (a: A), a ∈ t -> f1 a = ret (f2 a)) ->
      bind f1 t = map f2 t.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f1 : A -> T B) (f2 : A -> B)
  (t : T A),
(forall a : A, a ∈ t -> f1 a = ret (f2 a)) ->
bind f1 t = map f2 t
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A B : Type) (f1 : A -> T B) (f2 : A -> B)
  (t : T A),
(forall a : A, a ∈ t -> f1 a = ret (f2 a)) ->
bind f1 t = map f2 t
    introv hyp.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f1: A -> T B
f2: A -> B
t: T A
hyp: forall a : A, a ∈ t -> f1 a = ret (f2 a)
bind f1 t = map f2 t
    rewrite compat_map_bind.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A, B: Type
f1: A -> T B
f2: A -> B
t: T A
hyp: forall a : A, a ∈ t -> f1 a = ret (f2 a)
bind f1 t = DerivedOperations.Map_Bind T T A B f2 t
    now eapply bind_respectful.
  Qed.

  Corollary bind_respectful_id:
    forall `(f1: A -> T A) (t: T A),
      (forall (a: A), a ∈ t -> f1 a = ret a) -> bind f1 t = t.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (f1 : A -> T A) (t : T A),
(forall a : A, a ∈ t -> f1 a = ret a) -> bind f1 t = t
  Proof.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
forall (A : Type) (f1 : A -> T A) (t : T A),
(forall a : A, a ∈ t -> f1 a = ret a) -> bind f1 t = t
    introv hyp.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
f1: A -> T A
t: T A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = t
    change t with (id t) at 2.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
f1: A -> T A
t: T A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = id t
    rewrite <- kmon_bind1.
T: Type -> Type
H: Bind T T
H0: Return T
H1: ToSubset T
H2: ContainerMonad T
Map_inst: Map T
Compat_Map_Bind0: Compat_Map_Bind T T
A: Type
f1: A -> T A
t: T A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = bind ret t
    now apply bind_respectful.
  Qed.

End corollaries.

(** * Derived Properties of <<ContainerRightModule>> *)
(**********************************************************************)
Section corollaries.

  Context
    `{Return T}
    `{Module_inst: ContainerRightModule T U}
    `{Map_U_inst: Map U}
    `{! Compat_Map_Bind T U}.

  (** ** Specification of <<b ∈ bind f t>> *)
  (********************************************************************)
  Theorem mod_in_bind_iff:
    forall `(f: A -> T B) (t: U A) (b: B),
      b ∈ bind f t <-> exists a, a ∈ t /\ b ∈ f a.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f : A -> T B) (t : U A) (b : B),
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a)
  Proof.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f : A -> T B) (t : U A) (b : B),
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a)
    intros.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f: A -> T B
t: U A
b: B
b ∈ bind f t <-> (exists a : A, a ∈ t /\ b ∈ f a)
    compose near t on left.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f: A -> T B
t: U A
b: B
(element_of b ∘ bind f) t <->
(exists a : A, a ∈ t /\ b ∈ f a)
    rewrite element_of_tosubset.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f: A -> T B
t: U A
b: B
(evalAt b ∘ tosubset ∘ bind f) t <->
(exists a : A, a ∈ t /\ b ∈ f a)
    reassociate -> on left.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f: A -> T B
t: U A
b: B
(evalAt b ∘ (tosubset ∘ bind f)) t <->
(exists a : A, a ∈ t /\ b ∈ f a)
    rewrite (kmodpar_hom_bind (ϕ := @tosubset U _)).
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f: A -> T B
t: U A
b: B
(evalAt b ∘ (bind (tosubset ∘ f) ∘ tosubset)) t <->
(exists a : A, a ∈ t /\ b ∈ f a)
    reflexivity.
  Qed.

  (** ** Respectfulness Properties for <<bind>> *)
  (********************************************************************)
  Corollary mod_bind_respectful:
    forall (A B: Type) (t: U A) (f g: A -> T B),
      (forall a, a ∈ t -> f a = g a) -> bind f t = bind g t.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (t : U A) (f g : A -> T B),
(forall a : A, a ∈ t -> f a = g a) ->
bind f t = bind g t
  Proof.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (t : U A) (f g : A -> T B),
(forall a : A, a ∈ t -> f a = g a) ->
bind f t = bind g t
    apply contmod_pointwise.
  Qed.

  Corollary mod_bind_respectful_map:
    forall `(f1: A -> T B) `(f2: A -> B) (t: U A),
      (forall (a: A), a ∈ t -> f1 a = ret (f2 a)) ->
      bind f1 t = map f2 t.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f1 : A -> T B) (f2 : A -> B)
  (t : U A),
(forall a : A, a ∈ t -> f1 a = ret (f2 a)) ->
bind f1 t = map f2 t
  Proof.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A B : Type) (f1 : A -> T B) (f2 : A -> B)
  (t : U A),
(forall a : A, a ∈ t -> f1 a = ret (f2 a)) ->
bind f1 t = map f2 t
    introv hyp.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f1: A -> T B
f2: A -> B
t: U A
hyp: forall a : A, a ∈ t -> f1 a = ret (f2 a)
bind f1 t = map f2 t
    rewrite compat_map_bind.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A, B: Type
f1: A -> T B
f2: A -> B
t: U A
hyp: forall a : A, a ∈ t -> f1 a = ret (f2 a)
bind f1 t = DerivedOperations.Map_Bind T U A B f2 t
    now eapply mod_bind_respectful.
  Qed.

  Corollary mod_bind_respectful_id:
    forall `(f1: A -> T A) (t: U A),
      (forall (a: A), a ∈ t -> f1 a = ret a) ->
      bind f1 t = t.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A : Type) (f1 : A -> T A) (t : U A),
(forall a : A, a ∈ t -> f1 a = ret a) -> bind f1 t = t
  Proof.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
forall (A : Type) (f1 : A -> T A) (t : U A),
(forall a : A, a ∈ t -> f1 a = ret a) -> bind f1 t = t
    introv hyp.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A: Type
f1: A -> T A
t: U A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = t
    change t with (id t) at 2.
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A: Type
f1: A -> T A
t: U A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = id t
    rewrite <- (kmod_bind1 (U := U) (T := T)).
T: Type -> Type
H: Return T
U: Type -> Type
H0: Bind T T
H1: Bind T U
H2: Return T
H3: ToSubset T
H4: ToSubset U
Module_inst: ContainerRightModule T U
Map_U_inst: Map U
Compat_Map_Bind0: Compat_Map_Bind T U
A: Type
f1: A -> T A
t: U A
hyp: forall a : A, a ∈ t -> f1 a = ret a
bind f1 t = bind ret t
    now apply mod_bind_respectful.
  Qed.

End corollaries.