fix breakage from previous commit removing an unneeded hypothesis fro…

…m a lemma Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 2, 2024 · e38db3a · e38db3a
1 parent db02015
commit e38db3a
Showing 1 changed file with 0 additions and 2 deletions.
diff --git 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.