tc_error when rnd argument is present but unused

remove unneccessary argument in PRG example

Author: oskgo

examples/PRG.ec

@@ -337,7 +337,7 @@ section.
     inline Resample.resample Psample.init F.init.
     rcondf{2} 7;
       first by move=> &hr; rnd; wp; conseq (_: _ ==> true) => //.
-    by wp; rnd; wp; rnd{2} predT; auto; rewrite dseed_ll.
+    by wp; rnd; wp; rnd{2}; auto; rewrite dseed_ll.
   (* presampling ~ postsampling *)
   seq 2 2: (={glob A, glob F, glob Plog}); first by sim.
   eager (H: Resample.resample(); ~ Resample.resample();

src/phl/ecPhlRnd.ml

@@ -587,10 +587,10 @@ let wp_equiv_rnd_r bij tc =
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_rnd_r side pos bij_info tc =
-  match side, pos with
-  | Some side, None ->
+  match side, pos, bij_info with
+  | Some side, None, (None, None) ->
      wp_equiv_disj_rnd_r side tc
-  | None, _ -> begin
+  | None, _, _ -> begin
       let pos =
         match pos with
         | None -> None