diff --git a/coq/FIFO.v b/coq/FIFO.v
index e478a4f98dd567a2dbbe0c1968e9cb27510ebe31..4bd99a71692a73979254d3eaf455bf878529b1cb 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -291,15 +291,12 @@ Section FIFO.
 
   Program Definition FIFO_arbitrate :=
     let State := FIFO_trace Requests in
-      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) _ (FIFO_trace_T_RC_ok Requests) _.
-  Admit Obligations.
-
-  (*
+      mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_Cmds_PRE_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests).
   Next Obligation.
     induction Requests.
-    - auto. 
+    - auto.
     - by apply (FIFO_trace_uniq a) in IHl.
-  *)
+  Qed.
 
   Lemma FIFO_trace_Req_handled Reqs:
     forall req, req \in Reqs ->