From 4accfc913bb38e2f13c35c6dae77212be563e957 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Wed, 4 Dec 2024 18:08:05 -0500
Subject: [PATCH] Jaakkola_alpha_beta_unbounded_uniformly_W_alt

---
 coq/QLearn/jaakkola_vector.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
index 25b1ce74..fac3b189 100644
--- a/coq/QLearn/jaakkola_vector.v
+++ b/coq/QLearn/jaakkola_vector.v
@@ -7043,8 +7043,9 @@ Proof.
        eapply Rle_trans; cycle 1.
        apply H12.
        right.
-       admit.
+       f_equal.
+       apply proof_irrelevance.
    - trivial.               
-Admitted.
+ Qed.
 
 End jaakola_vector2.