diff --git a/coq/QLearn/qlearn_redux.v b/coq/QLearn/qlearn_redux.v
index 75ff8fab..2c0a87f1 100644
--- a/coq/QLearn/qlearn_redux.v
+++ b/coq/QLearn/qlearn_redux.v
@@ -2296,7 +2296,6 @@ Proof.
                  (g := const (Rbar.Finite A2)).
              - typeclasses eauto.
              - typeclasses eauto.
-             - typeclasses eauto.
              - revert alpha_sqr.
                apply almost_impl, all_almost.
                intros; red; intros.
@@ -2326,7 +2325,6 @@ Proof.
                  (g := const (Rbar.Finite A2)).
              - typeclasses eauto.
              - typeclasses eauto.
-             - typeclasses eauto.
              - revert alpha_sqr.
                apply almost_impl, all_almost.
                intros; red; intros.