diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index fd8e8d30..834847ba 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -1044,23 +1044,25 @@ Proof.
   - right; apply le_lt_eq ; now left. 
 Defined.
 
-
-Instance epsilon0_pre_order : TotalDecPreOrder (leq lt).
+Instance epsilon0_pre_order : TotalPreOrder (leq lt).
 Proof.
-  do 2 split.
+  split; [split|].
   - intro x; apply le_refl.
   - red; apply le_trans.
   - intros a b.
     destruct (lt_le_dec a b).
     + now do 2 left.
     + now right.
-  - intros a b.
-    destruct (lt_eq_lt_dec a b) as [[Hlt | Heq] | Hgt].
-    + now do 2 left.
-    + subst; now left; right.
-    + right; now apply lt_not_ge.
 Defined.
 
+Instance epsilon0_dec : RelDecision (leq lt).
+Proof.
+intros a b.
+destruct (lt_eq_lt_dec a b) as [[Hlt | Heq] | Hgt].
++ now do 2 left.
++ subst; now left; right.
++ right; now apply lt_not_ge.
+Defined.
 
 Ltac auto_nf :=
   match goal with
diff --git a/theories/ordinals/Prelude/DecPreOrder.v b/theories/ordinals/Prelude/DecPreOrder.v
index 5f63b453..84a0396b 100644
--- a/theories/ordinals/Prelude/DecPreOrder.v
+++ b/theories/ordinals/Prelude/DecPreOrder.v
@@ -8,28 +8,43 @@
 From Coq Require Export Relations RelationClasses Setoid.
 
 Class Total {A:Type}(R: relation A) :=
-  totalness : forall a b:A, R a b \/ R b a.             
+  totalness : forall a b:A, R a b \/ R b a.
 
-Class Decidable {A:Type}(R: relation A) :=
-  rel_dec : forall a b, {R a b} + {~ R a b}.
+(** Decision typeclasses following Spitters and van der Weegen *)
 
+Class Decision (P : Prop) := decide : {P} + {~P}.
+#[export] Hint Mode Decision ! : typeclass_instances.
+Arguments decide _ {_} : simpl never, assert.
+
+Class RelDecision {A B} (R : A -> B -> Prop) :=
+  decide_rel x y :> Decision (R x y).
+#[export] Hint Mode RelDecision ! ! ! : typeclass_instances.
+Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
+
+Notation EqDecision A := (RelDecision (@eq A)).
+
+Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
+  if dec then true else false.
 
 Instance Total_Reflexive{A:Type}{R: relation A}(rt : Total R):
   Reflexive R.
 Proof. intros a ; now destruct (rt a a). Qed.
 
+Module Semibundled.
+
 Class TotalDec {A:Type}(R: relation A):=
   { total_dec :> Total R ;
-    dec_dec :> Decidable R}.
-
-Definition left_right_dec {A:Type}{R: relation A}{T : Total R}{D: Decidable R}:
-  forall a b, {R a b}+{R b a}.
-Proof.  
-  intros a b; destruct (D a b).
-  - now left.
-  - right; destruct (T a b);[contradiction|trivial].
-Defined.
+    dec_dec :> RelDecision R}.
+
+(** A class of decidable total pre-orders *)
 
+Class TotalDecPreOrder {A:Type}(le: relation A) :=
+  {
+    total_dec_pre_order :> PreOrder le;
+    total_dec_total  :> TotalDec le
+  }.
+
+End Semibundled.
 
 (** when applied to a pre-order relation le, returns the equivalence and
     the strict order associated to le *)
@@ -40,15 +55,12 @@ Definition preorder_equiv {A:Type}{le:relation A} `{P:@PreOrder A le }(a b : A)
 Definition lt {A:Type}{le:relation A} `{P:@PreOrder A le }(a b : A) :=
   le a b /\ ~ le b a.
 
+(** A class of total pre-orders *)
 
-(** A class of decidable total pre-orders *)
-
-Class TotalDecPreOrder {A:Type}(le: relation A) :=
-  {
-    total_dec_pre_order :> PreOrder le;
-    total_dec_total  :> TotalDec le 
-  }.
-
+Class TotalPreOrder {A} (R : relation A) : Prop := {
+  total_pre_order_pre :> PreOrder R;
+  total_pre_order_total :> Total R
+}.
 
 (** Properties of decidable total pre-orders *)
 Lemma lt_irreflexive  {A:Type}{le:relation A}{P:PreOrder le}:
@@ -63,14 +75,14 @@ Proof.
    intros a b [H H0]; assumption.
 Qed.
 
-Lemma not_le_ge {A:Type}{le:relation A}{P0: TotalDecPreOrder le}:
-  forall a b,  ~ le  a b ->  le b a.
+Lemma not_le_ge {A} {le:relation A} {P0 : TotalPreOrder le} :
+  forall a b, ~ le a b -> le b a.
 Proof.
-  intros a b H; destruct P0. destruct (left_right_dec b a).
+  intros a b H. destruct P0.
+  destruct (totalness a b).
+  - contradiction.
   - assumption.
-  -  contradiction.
-Qed.  
-
+Qed.
 
 Lemma le_not_gt {A:Type}{le:relation A}{P:PreOrder le}:
   forall a b,  le  a b -> ~ lt b a.
@@ -129,74 +141,19 @@ split.
 - intros x y z Hxy Hyz; destruct Hxy, Hyz; split; transitivity y;auto.
 Qed.
 
-(** weakening of le_dec *)
-
-Definition leb {A:Type}(le : relation A)
-      {P0: TotalDecPreOrder le} (a b : A) :=
-   if rel_dec a b then true else false.
-
-Lemma leb_true {A:Type}(le : relation A)
-      (P0: TotalDecPreOrder le) (a b:A) :
-  leb le a b = true <-> le a b.
+Lemma le_lt_equiv_dec  {A:Type} {le : relation A}
+ {P0: TotalPreOrder le} {dec : RelDecision le} (a b:A) :
+ le a b -> {lt a b}+{preorder_equiv a b}.
 Proof.
-  unfold leb;split.
-  -   destruct (rel_dec a b);auto; discriminate.
-  -  intro;  destruct (rel_dec a b);auto.
-      contradiction.
-Qed.   
-
-(** if Hle assumes (le a b), asserts  (H: leb le a b = true) *)
-
-Ltac le_2_leb  Hle H:=
-  match goal with [Q : @TotalDecPreOrder ?A ?R, Hle: ?R ?x ?b |- _] => 
-                  let HH := fresh in
-                  let hypo := fresh H in
-                  destruct (@leb_true _ _ Q x b ) as
-                      [_ HH]; generalize (HH Hle); clear HH; intro  hypo
-  end.
-
-(** if Hlen assumes (leb a b = true), asserts  (H: le a b ) *)
-
-Ltac leb_2_le Hleb H:=
- match goal with [Q : @TotalDecPreOrder ?A ?R,
-                      Hleb : @leb ?A ?R ?Q ?x ?b = true |- _] => 
-                 let HH := fresh in
-                 let hypo := fresh H in
-                 destruct (@leb_true _ _ Q x b ) as
-                     [HH _]; generalize (HH Hleb); clear HH; intro  hypo
- end.
-
-
-Lemma leb_false {A:Type}(le : relation A)
-      (P0: TotalDecPreOrder le) (a b:A) :
-  leb le a b = false <-> lt  b a.
-Proof.
-  unfold leb, lt;split.
-  -   destruct (rel_dec a b);auto.  
-      + discriminate.
-      +   intros _; destruct (rel_dec b a); auto.
-          split;auto.
-          { destruct (left_right_dec a b);try contradiction. }
-  -  destruct (rel_dec a b).
-     + destruct 1; contradiction.   
-     +   auto . 
-Qed.   
-
-
-Lemma le_lt_equiv_dec  {A:Type}(le : relation A)
-      (P0: TotalDecPreOrder le) (a b:A) :
-   le a b -> {lt a b}+{preorder_equiv a b}.
-Proof.
-  intro H;  destruct (rel_dec b a).
- -   right;split;auto.
- -  left;split;auto.
+  intro H; destruct (decide (le b a)).
+  - right;split;auto.
+  - left;split;auto.
 Defined.
 
-
 Lemma not_le_gt {A:Type}(le : relation A)
-      (P0: TotalDecPreOrder le) (a b:A) : ~ le a b -> lt b a.
+      (P0: TotalPreOrder le) (a b:A) : ~ le a b -> lt b a.
 Proof.
-  intro H; destruct (left_right_dec b a).
+  intro H. destruct (totalness b a).
   - split; auto.   
   - contradiction.
 Qed.
diff --git a/theories/ordinals/Prelude/DecPreOrder_Instances.v b/theories/ordinals/Prelude/DecPreOrder_Instances.v
index ff9a9508..9351028d 100644
--- a/theories/ordinals/Prelude/DecPreOrder_Instances.v
+++ b/theories/ordinals/Prelude/DecPreOrder_Instances.v
@@ -3,24 +3,24 @@
 From hydras Require Export DecPreOrder.
 From Coq Require Import Arith ZArith List  Sets.Finite_sets  Sets.Ensembles.
 
-Instance Nat_le_TO : TotalDecPreOrder le .
+Instance Nat_le_dec : RelDecision le := le_dec.
+
+Instance Nat_le_TO : TotalPreOrder le.
 Proof.
  split.
  - apply Nat.le_preorder.
- - split.
- + intros a b; apply Nat.le_ge_cases. 
- + intros a b; apply le_dec. 
-Defined.
+ - intros a b; apply Nat.le_ge_cases.
+Qed.
 
-Instance Z_le_TO : TotalDecPreOrder Z.le .
-split. 
+Instance Z_le_dec : RelDecision Z.le := Z_le_dec.
+
+Instance Z_le_TO : TotalPreOrder Z.le.
+split.
 - apply Z.le_preorder.
-- split.
-  + intros a b; destruct (Z_le_gt_dec a b).
+- intros a b; destruct (Z_le_gt_dec a b).
     *  left;auto.
     *  right; auto with zarith.
- + intros a b;apply  Z_le_dec.   
-Defined.
+Qed.
 
 Import DecPreOrder.
 
@@ -36,20 +36,23 @@ Proof.
 Defined.
 
 
-Instance TotalDec_Inverse_fun {A B:Type}{f : A -> B}
-         {leB: relation B}{TB: TotalDecPreOrder leB} :
-                     TotalDecPreOrder (fun x y => leB (f x) (f y)).
+Instance Total_Inverse_fun {A B:Type}{f : A -> B}
+         {leB: relation B}{TB: TotalPreOrder leB} :
+                     TotalPreOrder (fun x y => leB (f x) (f y)).
 Proof.
 split.
 - apply Inverse_fun.
--  split. intros a b; destruct (left_right_dec (f a) (f b)).
+- intros a b.
+  destruct TB.
+  destruct (total_pre_order_total (f a) (f b)).
   + now left.
   + now right.
-  +   intros a b; destruct (dec_dec (f a) (f b)). 
-  *  now left.
-  * now right.
 Defined.
 
+Instance RelDecision_Inverse_fun {A B:Type}{f : A -> B}
+ {leB: relation B} {RDB : RelDecision leB} :
+  RelDecision (fun x y => leB (f x) (f y)) :=
+  fun x y => decide_rel leB (f x) (f y).
 
 (** Pre-order associated with inclusion *)
 
@@ -72,8 +75,8 @@ Infix "'<s'" := Included_s (at level 30).
   Lists (pre-ordered by their length) *)
 
 Instance  List_length {A:Type}: 
-   TotalDecPreOrder (fun l l' : list A => List.length l <= List.length l')%nat.
-apply TotalDec_Inverse_fun.
+   TotalPreOrder (fun l l' : list A => List.length l <= List.length l')%nat.
+apply Total_Inverse_fun.
 Defined.
 
 (** Non dependent lexicographic product *)
@@ -82,11 +85,13 @@ Section lexprod.
  Variables (A B : Type)
            (leA : relation A) 
            (leB : relation B).
- Context (TA : TotalDecPreOrder leA)
-         (TB : TotalDecPreOrder leB).
+ Context (TA : TotalPreOrder leA)
+         (TB : TotalPreOrder leB)
+         (DA : RelDecision leA)
+         (DB : RelDecision leB).
  
- Definition PA := @total_dec_pre_order A leA TA. 
- Definition PB := @total_dec_pre_order B leB TB.
+ Definition PA := @total_pre_order_pre A leA TA.
+ Definition PB := @total_pre_order_pre B leB TB.
  
  
 Notation "x '<=A' y" := (leA x y) (at level 70, no associativity).
@@ -172,54 +177,55 @@ Proof.
   apply (@lt_irreflexive _ _ PA a).
   apply DecPreOrder.lt_le_trans with a'; auto.
   apply (lex_inv_left _ _ _ _ H0).
-Qed. 
-
+Qed.
 
-Global Instance To_lex_prod : TotalDecPreOrder lex_prod.
+Global Instance To_lex_prod : TotalPreOrder lex_prod.
 Proof.
   split.
   - apply PO_lex_prod.
-  -  split.
-  
-  +  intros x y; destruct x, y.
-     destruct (left_right_dec a a0).
-     * destruct (le_lt_equiv_dec _ _ a a0 l). 
-       { left;left;auto. }
-       { destruct (left_right_dec b b0).
-         { left;right;auto. }
-         { right; right;  simpl. now symmetry.
-           assumption.
-         }
-       }
-     *  destruct (le_lt_equiv_dec _ _ a0 a l). 
-        {  right;left. assumption.  }
-        { destruct (left_right_dec b0 b).
-           right; right;  simpl;  assumption. 
-           left;  right;[ now symmetry | assumption].
-        }
-  + intros x y; destruct x, y.
-    destruct (dec_dec a a0).
-    *  destruct (le_lt_equiv_dec _ _ a a0 l).
-       {     left;  left.   simpl. apply l0. }
-       {   destruct (dec_dec b b0).
-           {  left;auto.
-              constructor 2; simpl;auto.
-           }
-           {
-             right.      
-             inversion 1.
-             simpl in H0.
-             now destruct (equiv_not_lt  _ _  p).
-             simpl in *.
-             contradiction.
-           }
-       }
-    * right.
-      inversion 1.
-      simpl in H0.
-      destruct n;now apply le_lt_weak.
-      simpl in H0;destruct H0.
-      contradiction.
+  - destruct TA as [Apre Atot].
+    destruct TB as [Bpre Btot].
+    intros x y; destruct x, y.
+    destruct (Atot a a0) as [HAle|HAle].
+    * destruct (le_lt_equiv_dec a a0 HAle) as [Ha|Ha].
+      + left;left;auto.
+      + destruct (Btot b b0).
+        { left;right;auto. }
+        { right; right; simpl. now symmetry. assumption. }
+    * destruct (le_lt_equiv_dec a0 a HAle).
+      + right;left. assumption.
+      + destruct (Btot b0 b).
+        { right; right; simpl; assumption. }
+        { left;  right;[ now symmetry | assumption]. }
+Qed.
+
+Global Instance lex_prod_dec : RelDecision lex_prod.
+Proof.
+intros x y; destruct x, y.
+destruct (decide (leA a a0)) as [HAle|Hale].
+- destruct (le_lt_equiv_dec a a0 HAle) as [Ha|Ha].
+  * left;left;auto.
+  * destruct (decide (leB b b0)) as [HBle|HBle].
+    + left;right;auto.
+    + right; intro Hle.
+      contradict HBle.
+      destruct Hle as [Hle|Hle].
+      { simpl in Hle.
+        destruct Ha.
+        destruct Hle.
+        contradiction. }
+      { simpl in Hle.
+        simpl in H.
+        assumption. }
+- right. intro Hle.
+  destruct Hle as [Hle|Hle].
+  * simpl in Hle.
+    destruct Hle.
+    contradiction.
+  * simpl in Hle.
+    contradict Hale.
+    destruct Hle.
+    assumption.
 Defined.
 
 End lexprod.
diff --git a/theories/ordinals/Prelude/Merge_Sort.v b/theories/ordinals/Prelude/Merge_Sort.v
index e212d7bc..21af2d57 100644
--- a/theories/ordinals/Prelude/Merge_Sort.v
+++ b/theories/ordinals/Prelude/Merge_Sort.v
@@ -156,36 +156,33 @@ Section Generic.
 
     Variable le : relation A.
 
-    Context (le_total : TotalDecPreOrder le ).
+    Context (le_total : TotalPreOrder le).
+    Context (le_dec : RelDecision le).
 
     Notation "a <= b" := (le a b).
-    Notation "a <=? b" := (leb le a b).
 
     Lemma merge_rect:
       forall P: list A -> list A -> list A -> Type,
         (forall l:list A, P nil l l) ->
         (forall l: list A, P l nil l) ->
-        (forall a1 l1 a2 l2 p,
-           dec_dec a1 a2 = left p ->
-           P l1 (a2::l2) (merge (leb le) l1 (a2::l2)) ->
-           P (a1::l1) (a2::l2) (a1::(merge (leb le)l1 (a2::l2)))) ->
-        (forall a1 l1 a2 l2 p,
-           dec_dec a1 a2 = right p ->
-           P (a1::l1) l2 (merge (leb le)(a1::l1) l2) ->
-           P (a1::l1) (a2::l2) (a2::(merge (leb le) (a1::l1) l2))) ->
-        forall l1 l2, P l1 l2 (merge (leb le) l1 l2).
+        (forall a1 l1 a2 l2,
+           a1 <= a2 ->
+           P l1 (a2::l2) (merge (fun x y => bool_decide (x <= y)) l1 (a2::l2)) ->
+           P (a1::l1) (a2::l2) (a1::(merge (fun x y => bool_decide (x <= y))l1 (a2::l2)))) ->
+        (forall a1 l1 a2 l2,
+           ~ le a1 a2 ->
+           P (a1::l1) l2 (merge (fun x y => bool_decide (x <= y))(a1::l1) l2) ->
+           P (a1::l1) (a2::l2) (a2::(merge (fun x y => bool_decide (x <= y)) (a1::l1) l2))) ->
+        forall l1 l2, P l1 l2 (merge (fun x y => bool_decide (x <= y)) l1 l2).
     Proof with auto.
       induction l1.
       - intros; simpl; destruct  l2; apply X.
       - induction l2.
         + apply X0.
-        + case_eq (dec_dec a a0); intros Eq Comp.
-          * simpl. le_2_leb Eq H1. rewrite H1; simpl.
-            eapply X1.   eexact Comp. apply IHl1.  
-          * simpl.  assert (a <=? a0 = false).
-            rewrite  leb_false.
-            apply not_le_gt; auto.
-            rewrite H.  eapply X2;eauto. 
+        + simpl; unfold bool_decide.
+          destruct (decide_rel le a a0).
+          * apply X1; [assumption|apply IHl1].
+          * apply X2; assumption.
     Qed.
 
     Definition merge_ind ( P: list A -> list A -> list A -> Prop) :=
@@ -195,24 +192,26 @@ Section Generic.
       merge_rect P.
 
 
-    Ltac induction_merge l1 l2:= pattern (merge (leb le) l1 l2 ); apply merge_rect.
+    Ltac induction_merge l1 l2:= pattern (merge (fun x y => bool_decide (x <= y)) l1 l2 ); apply merge_rect.
     
     Lemma merge_equation:
       forall l1 l2,
-        merge (leb le) l1 l2 =
+        merge (fun x y => bool_decide (x <= y)) l1 l2 =
         match l1,l2 with
           | nil,_ => l2
           | _,nil => l1
           | a1::l1',a2::l2' =>
-            if dec_dec a1  a2 then a1 :: merge (leb le) l1' l2
-            else a2 :: merge (leb le) l1 l2'
+            if decide (a1 <= a2) then a1 :: merge (fun x y => bool_decide (x <= y)) l1' l2
+            else a2 :: merge (fun x y => bool_decide (x <= y)) l1 l2'
         end.
     Proof.
       intros l1 l2.
       induction_merge l1 l2; trivial.
       - now intros l; destruct l.
-      - intros a1 l1' a2 l2' Comp Eq .  rewrite Eq; reflexivity.
-      - intros a1 l1' a2 l2' Comp Eq; rewrite Eq; reflexivity.
+      - intros a1 l1' a2 l2' Comp Eq.
+        destruct (decide (a1 <= a2)); [reflexivity|contradiction].
+      - intros a1 l1' a2 l2' Comp Eq.
+        destruct (decide (a1 <= a2)); [contradiction|reflexivity].
     Qed.
 
 
@@ -226,7 +225,7 @@ Section Generic.
         forall  (f:A->Prop) l1 l2,
           List.Forall f l1 ->
           List.Forall f l2  ->
-          List.Forall f (merge (leb le) l1 l2) .
+          List.Forall f (merge (fun x y => bool_decide (x <= y)) l1 l2) .
       Proof with auto.
         intros f l1 l2.
         induction_merge l1 l2; intros ...
@@ -239,7 +238,7 @@ Section Generic.
 
       Lemma merge_LocallySorted:
         forall l1 l2, LocallySorted  le l1 -> LocallySorted le  l2 ->
-                      LocallySorted le (merge (leb le) l1 l2).
+                      LocallySorted le (merge (fun x y => bool_decide (x <= y)) l1 l2).
       Proof with auto.
         intros l1 l2; induction_merge l1 l2; intros ...
         - rewrite <- (LocallySorted_cons' A le).
@@ -269,7 +268,7 @@ Section Generic.
 Qed.
 
       Lemma merge_permutation:
-        forall l1 l2, Permutation (l1++l2) (merge (leb le) l1 l2).
+        forall l1 l2, Permutation (l1++l2) (merge (fun x y => bool_decide (x <= y)) l1 l2).
       Proof with auto.
         intros l1 l2;  induction_merge l1 l2; intros. 
         - reflexivity.
@@ -311,20 +310,20 @@ Qed.
           now rewrite teq1.
         Defined.
         
-        Theorem merge_sort_correct: sort_correct A le (merge_sort (leb le)).
+        Theorem merge_sort_correct: sort_correct A le (merge_sort (fun x y => bool_decide (x <= y))).
         Proof with auto with lists.
-          intro l;   functional induction (merge_sort (leb le) l) ...
+          intro l;   functional induction (merge_sort (fun x y => bool_decide (x <= y)) l) ...
           - split...
           - split ...      
           -  destruct IHl0, IHl1. split ...
-             apply (merge_LocallySorted (merge_sort (leb le) l1)
-                                        (merge_sort (leb le) l2)); trivial.
+             apply (merge_LocallySorted (merge_sort (fun x y => bool_decide (x <= y)) l1)
+                                        (merge_sort (fun x y => bool_decide (x <= y)) l2)); trivial.
              transitivity (l1++l2).
              generalize (split_permutation (_x :: _x0 :: _x1)).
              rewrite e0.
              intro;symmetry...       
-             transitivity ((merge_sort (leb le) l1)
-                             ++ (merge_sort (leb le) l2)).
+             transitivity ((merge_sort (fun x y => bool_decide (x <= y)) l1)
+                             ++ (merge_sort (fun x y => bool_decide (x <= y)) l2)).
              rewrite <- H0, <- H2 ...
              apply merge_permutation; trivial.
         Qed.
@@ -346,7 +345,7 @@ Check (stable_merge_sort: sort_fun_t).
 
 Theorem sp_mergesort_OK : sort_spec sp_merge_sort.
 Proof.
-  red; intros.  now destruct  (merge_sort_correct A le P
+  red; intros.  now destruct  (merge_sort_correct A le P _
                                                   (split _) (split_decr _)
                                                   (split_permutation _)
                                                   l).
@@ -354,7 +353,7 @@ Qed.
 
 Theorem stable_mergesort_OK : sort_spec stable_merge_sort.
 Proof.
-  red; intros.  now destruct  (merge_sort_correct A le P
+  red; intros.  now destruct  (merge_sort_correct A le P _
                                                   (split' _) (split'_decr _)
                                                   (split'_permutation _)
                                                   l).
diff --git a/theories/ordinals/Prelude/Sort_spec.v b/theories/ordinals/Prelude/Sort_spec.v
index 44be060b..0aa5f97c 100644
--- a/theories/ordinals/Prelude/Sort_spec.v
+++ b/theories/ordinals/Prelude/Sort_spec.v
@@ -132,16 +132,15 @@ Global Hint Constructors LocallySorted : lists.
 (** A sort must work on any decidable total pre-order *)
 
 Definition sort_spec (f : sort_fun_t) :=
-forall  (A:Type)(le:relation A)(P:TotalDecPreOrder le)
-        (l:list A),
-    let l' := f A (leb le) l in Permutation l l' /\ LocallySorted le l'.
+ forall (A:Type) (le:relation A) (P:TotalPreOrder le) (dec:RelDecision le) (l:list A),
+ let l' := f A (fun x y => bool_decide (le x y)) l in Permutation l l' /\ LocallySorted le l'.
 
 (** A prototype for using TotalDecPreOrder type class *)
 
 Definition sort (f:sort_fun_t)
-           {A} {le : relation A}{P: TotalDecPreOrder le}
-           (l: list A) :=
-  f A (leb le) l.
+ {A} {le : relation A} {P: TotalPreOrder le} {dec:RelDecision le}
+ (l: list A) :=
+  f A (fun x y => bool_decide (le x y)) l.
 
 
 
@@ -157,15 +156,12 @@ list (A * B) -> Prop :=
                            leA a a' -> lt  b b') ->
             marked leA leB ((a,b)::l).
 
-
-
 Definition stable (f : sort_fun_t) : Prop :=
-  forall (A B : Type) leA leB (PA : TotalDecPreOrder leA)
-         (PB : TotalDecPreOrder leB)
-         (l : list (A * B)),
+  forall (A B : Type) leA leB
+    (PA : TotalPreOrder leA) (PB : TotalPreOrder leB)
+    (dec : RelDecision leA) (l : list (A * B)),
          marked leA leB l ->
-         marked leA  leB
-                (sort f  (P:= TotalDec_Inverse_fun
+         marked leA leB (sort f  (P:= Total_Inverse_fun
                                 (f:= fst : A * B -> A))
                       l).
                            
@@ -179,10 +175,10 @@ end.
 
 
 Definition stable_test (f : sort_fun_t)
-      {A} {le : relation A}{P: TotalDecPreOrder le}
+      {A} {le : relation A}{P: TotalPreOrder le} {dec:RelDecision le}
            (l: list A) : list (A  * nat)                                                               :=
     let m := mark l 0 in
-      sort f  (P:= @TotalDec_Inverse_fun (A * nat) A fst le P) m. 
+      sort f  (P:= @Total_Inverse_fun (A * nat) A fst le P) m.