made proph_extract_winner only consider the first value in the list

theories/logatom/rdcss/rdcss.v

@@ -161,7 +161,6 @@ Section rdcss.
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
     | ((_, #true)%V, LitV (LitProphecy p)) :: _  => Some p
-    | _                         :: vs => proph_extract_winner vs
     | _                               => None
     end.