Remove unused lemma

README.md

@@ -115,6 +115,7 @@ for testing.
 
     + `Monad`: Properties of monads (in the category of functions).
     + `MonadState`: The state monad transformer.
+    + `MonadProp`: The nondeterminism monad.
 
 - `Core`: Main definitions for interaction trees.
 

theories/Basics/Basics.v

@@ -3,7 +3,7 @@
 (** Not specific to itrees. *)
 
 (* begin hide *)
-From Coq Require 
+From Coq Require
      Ensembles.
 
 From Coq Require Import
@@ -77,10 +77,10 @@ Section ProdRelInstances.
   Proof.
     red. destruct x. constructor; auto.
   Qed.
-  
+
   Global Instance prod_rel_sym `{Symmetric _ RR} `{Symmetric _ SS}  : Symmetric (prod_rel RR SS).
   Proof.
-    red. intros. 
+    red. intros.
     inversion H1. subst.
     constructor; symmetry; auto.
   Qed.

theories/Basics/MonadProp.v

@@ -19,7 +19,7 @@ Local Open Scope cat_scope.
 Local Open Scope cat.
 
 Section prop.
-  Global Instance Monad_Prop : Monad Ensembles.Ensemble :=
+  Global Instance Monad_Prop : Monad Ensemble :=
     {|
     ret := fun _ x y => x = y;
     bind := fun _ _ Pa K b => exists a, In _ Pa a /\ In _ (K a) b
@@ -35,16 +35,6 @@ Section prop.
     - repeat intro. destruct H, H0. split; repeat intro; auto.
   Qed.
 
-  Lemma bind_bind_Prop :
-    forall A B C (Pa : Ensembles.Ensemble A)
-      (f : A -> Ensembles.Ensemble B) (g : B -> Ensembles.Ensemble C),
-      eqm (bind (bind Pa f) g) (bind Pa (fun y => bind (f y) g)).
-  Proof.
-    intros. split; repeat intro; simpl in *;
-              [destruct H as (? & (? & ? & ?) & ?) | destruct H as (? & ? & (? & ? & ?))];
-              do 2 (eexists; split; eauto).
-  Qed.
-
   Instance MonadLaws_Prop : MonadLaws Ensemble.
   Proof.
     constructor.