diff --git a/theories/ordinals/Prelude/Merge_Sort.v b/theories/ordinals/Prelude/Merge_Sort.v
index 13e415cc..b05308eb 100644
--- a/theories/ordinals/Prelude/Merge_Sort.v
+++ b/theories/ordinals/Prelude/Merge_Sort.v
@@ -244,15 +244,18 @@ Section Generic.
         - rewrite <- (LocallySorted_cons' A le).
           split.
           + apply (merge_Forall (le a1) l0 (a2::l3)).
-            * rewrite <- LocallySorted_cons' in H1; intuition.
-            * rewrite <- LocallySorted_cons' in H2; intuition.
+            * rewrite <- LocallySorted_cons' in H1. 
+              now destruct H1.
+              apply le_total.
+            * rewrite <- LocallySorted_cons' in H2. 
+              intuition.
               apply forall_weak with a2 ...
+              apply le_total. intuition.
               apply le_total.
-              now constructor.
           + eapply H0 ...
             rewrite <- LocallySorted_cons' in H1; intuition.
           + apply le_total.
-- rewrite <- LocallySorted_cons'.
+        - rewrite <- LocallySorted_cons'.
           split.
           +  apply (merge_Forall (le a2) (a1::l0) l3).
              * rewrite <- LocallySorted_cons' in H1; intuition.
@@ -264,8 +267,8 @@ Section Generic.
              * rewrite <- LocallySorted_cons' in H2; intuition.
           +  eapply H0 ...
              rewrite <- LocallySorted_cons' in H2; intuition.
-      + apply le_total.
-Qed.
+          + apply le_total.
+      Qed.
 
       Lemma merge_permutation:
         forall l1 l2, Permutation (l1++l2) (merge (fun x y => bool_decide (x <= y)) l1 l2).
diff --git a/theories/ordinals/Schutte/Schutte_basics.v b/theories/ordinals/Schutte/Schutte_basics.v
index c26f2335..3f9e860e 100644
--- a/theories/ordinals/Schutte/Schutte_basics.v
+++ b/theories/ordinals/Schutte/Schutte_basics.v
@@ -475,7 +475,8 @@ Proof. (* .no-out *)
   (*| .. coq:: no-out |*)
   destruct (@AX3 (Singleton alpha)).
   - apply countable_singleton.
-  - unfold succ_spec; apply the_least_unicity; exists x; intuition.
+  - unfold succ_spec; apply the_least_unicity; exists x. 
+    apply H; split. 
 Qed.
 (*||*)
 (* end snippet succOkb *)