Continuation change, extract_proph_winner change

The continuation Q is moved to the top level in the Accepted state.

extract_proph_winner now only considers the first element in the list and does not restrict the first value.

theories/logatom/rdcss/rdcss.v

@@ -158,5+158,5 @@
   Qed.
 
   Definition rdcss_content (γ_n : gname) (n : val) := (own γ_n (◯ Excl' n))%I.
 
   (** Definition of the invariant *)
 
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
-    | ((_, #true)%V, LitV (LitProphecy tid)) :: _  => Some tid
+    | ((_, _)%V, LitV (LitProphecy tid)) :: _  => Some tid
     | _                               => None
     end.