diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca
index 8725b35214..4de755096e 100644
--- a/theories/crypto/PRF.eca
+++ b/theories/crypto/PRF.eca
@@ -57,30 +57,23 @@ end RF.
 abstract theory PseudoRF.
 type K.
 
-op dK: { K distr | is_lossless dK } as dK_ll.
-
-op F : K -> D -> R.
-
 module type PseudoRF = {
   proc keygen(): K
-  proc f(_ : K * D): R
+  proc f(_: K * D): R
 }.
 
-module PseudoRF = {
-  proc keygen() = {
-    var k;
+module PRF (P : PseudoRF) = {
+  var k : K
 
-    k <$ dK;
-    return k;
+  proc init() = {
+    k <@ P.keygen();
   }
 
-  proc f(k, x) = { return F k x; }
-}.
-
-module PRF = {
-  var k : K
+  proc f(x: D) = {
+    var r;
 
-  proc init() = { k <$ dK; }
-  proc f(x: D) = { return F k x; }
+    r <@ P.f(k, x);
+    return r;
+  }
 }.
 end PseudoRF.
diff --git a/theories/crypto/prp_prf/RP_RF.eca b/theories/crypto/prp_prf/RP_RF.eca
new file mode 100644
index 0000000000..5247596981
--- /dev/null
+++ b/theories/crypto/prp_prf/RP_RF.eca
@@ -0,0 +1,307 @@
+require import AllCore Distr List FSet FMap.
+require import Dexcepted.
+require (*--*) PRP.
+(*---*) import RField StdOrder.RealOrder.
+
+require (*--*) FelTactic.
+
+(** We assume a finite domain D, equipped with a full and lossless
+distribution. (We need fullness and losslessness to know that
+resampling always works.) **)
+type D.
+
+op [lossless full] dD: D distr.
+op hmin_dD: { real | forall x, mu1 dD x <= hmin_dD } as hmin_dDP.
+
+lemma ge0_hmin_dD: 0%r <= hmin_dD.
+proof.
+apply: (ler_trans (mu1 dD witness)).
++ exact: ge0_mu.
+exact: hmin_dDP.
+qed.
+
+(** and a type K equipped with a lossless distribution **)
+type K.
+
+clone import PRP as PRPt with
+  type D  <- D
+proof *.
+
+clone import StrongPRP as PRPSec
+proof *.
+
+clone import RP as PRPi with
+    op dD <- dD
+proof *
+rename "RP" as "PRPi".
+realize dD_ll by exact: dD_ll.
+
+clone import PRF as PRFt with
+  type D <- D,
+  type R <- D
+proof *.
+
+clone import RF with
+  op dR _ <- dD
+proof *
+rename "RF" as "PRFi".
+realize dR_ll by rewrite dD_ll.
+
+module Count (P: PRF): PRF = {
+  var count: int
+
+  proc init() = {
+    P.init();
+    count <- 0;
+  }
+
+  proc f(x) = {
+    var r;
+
+    r <@ P.f(x);
+    count <- count + 1;
+    return r;
+  }
+}.
+
+section.
+
+(** The following is a proof that holds **)
+(** For all lossless distinguisher D ... **)
+declare module D <: Distinguisher { -PRPi, -PRFi, -Count }.
+declare axiom D_ll (O <: PRF_Oracles {-D}): islossless O.f => islossless D(O).distinguish.
+
+(** ... that makes at most q queries for some non-negative q. **)
+declare op q : { int | 0 <= q } as ge0_q.
+declare axiom D_count (O <: PRF { -D, -Count }) c0:
+  hoare [D(Count(O)).distinguish: Count.count = c0 ==> Count.count <= c0 + q].
+
+(** We make use of a generic principle for sampling in a conditional
+    distribution **)
+local clone import TwoStepSampling with
+  type i    <- unit,
+  type t    <- D,
+  op   dt _ <- dD
+proof *.
+
+(** And we put some work into turning our random function (PRFi) and
+    random permutation (PRPi) into part of a distinguisher against a
+    sampling procedure. **)
+local module type Sample_t = {
+  proc sample(X: D -> bool): D
+}.
+
+local module Direct : Sample_t = {
+  proc sample(X) = {
+    var r;
+
+    r <@ S.direct((), fun _=> X);
+    return r;
+  }
+}.
+
+local module Indirect : Sample_t = {
+  proc sample(X) = {
+    var r;
+
+    r <@ S.indirect((), fun _=> X);
+    return r;
+  }
+}.
+
+local equiv eq_Direct_Indirect:
+  Direct.sample ~ Indirect.sample: ={X} ==> ={res}.
+proof.
+by proc; call ll_direct_indirect_eq; auto; rewrite dD_ll.
+qed.
+
+local module PRPi' (S:Sample_t) = {
+  proc init = PRPi.init
+
+  proc f(x:D): D = {
+    var r;
+    if (x \notin PRPi.m) {
+      r <@ S.sample(rng PRPi.m);
+      PRPi.m.[x] <- r;
+    }
+    return oget PRPi.m.[x];
+  }
+}.
+
+(* We need bad flags *)
+local module PRFi'_bad = {
+  var bad: bool
+
+  proc init() = {
+    PRPi.init();
+    bad <- false;
+  }
+
+  proc f(x: D): D = {
+    var r;
+
+    if (x \notin PRPi.m) {
+      r <$ dD;
+      bad <- bad \/ rng PRPi.m r;
+      PRPi.m.[x] <- r;
+    }
+    return oget PRPi.m.[x];
+  }
+}.
+
+local module PRPi'_bad = {
+  proc init() = {
+    PRPi.init();
+    PRFi'_bad.bad <- false;
+  }
+
+  proc f(x: D): D = {
+    var r;
+
+    if (x \notin PRPi.m) {
+      r <$ dD;
+      if (rng PRPi.m r) {
+        PRFi'_bad.bad <- true;
+        r <$ dD \ (rng PRPi.m);
+      }
+      PRPi.m.[x] <- r;
+    }
+    return oget PRPi.m.[x];
+  }
+}.
+
+(* FIXME: lift out and share with Strong RP RF *)
+local lemma notin_supportIP (P : 'a -> bool) (d : 'a distr):
+  (exists a, support d a /\ !P a) <=> mu d P < mu d predT.
+proof.
+rewrite (mu_split _ predT P) /predI /predT /predC /=.
+rewrite (exists_eq (fun a => support d a /\ !P a) (fun a => !P a /\ a \in d)) /=.
++ by move=> a /=; rewrite andbC.
+by rewrite -(witness_support (predC P)) -/(predC _) /#.
+qed.
+
+local lemma excepted_lossless (m:(D,D) fmap):
+  (exists x, x \notin m) =>
+  mu (dD \ (rng m)) predT = 1%r.
+proof. 
+move=> /endo_dom_rng [x h]; rewrite dexcepted_ll // 1:dD_ll.
+by rewrite -dD_ll; apply: notin_supportIP; exists x; rewrite dD_fu.
+qed.
+
+(** We split this into extremely small steps, but this is not
+    necessary **)
+local lemma pr_PRPi_PRPi'_Direct &m:
+    Pr[IND(PRPi, D).main() @ &m: res]
+  = Pr[IND(PRPi'(Direct), D).main() @ &m:res].
+proof.
+byequiv=> //; proc; call (: ={PRPi.m}).
++ by proc; if=> //; inline *; auto.
+by inline *; auto.
+qed.
+
+local lemma pr_PRPi'_Direct_PRPi'_Indirect &m:
+    Pr[IND(PRPi'(Direct), D).main() @ &m: res]
+  = Pr[IND(PRPi'(Indirect), D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={PRPi.m}).
++ proc; if=> //; auto.
+  by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll.
+by inline *; auto.
+qed.
+
+local lemma pr_PRPi'_Indirect_PRPi'_bad &m:
+    Pr[IND(PRPi'(Indirect), D).main() @ &m: res]
+  = Pr[IND(PRPi'_bad, D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={PRPi.m}).
++ proc; if=> //; inline *.
+  do ! cfold {1} 1.
+  seq 1 1: (#pre /\ r1{1} = r{2}); 1:by auto.
+  by if=> //; auto.
+by inline *; auto.
+qed.
+
+local lemma pr_PRFi'_PRFi &m:
+    Pr[IND(PRFi, D).main() @ &m: res]
+  = Pr[IND(PRFi'_bad, D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={m}(PRFi, PRPi)); 1:by sim.
+by inline *; auto.
+qed.
+
+local lemma pr_PRPi'_Indirect_PRFi &m:
+     `|  Pr[IND(PRPi'_bad, D).main() @ &m: res]
+       - Pr[IND(PRFi, D).main() @ &m: res]|
+  <= Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad].
+proof.
+rewrite pr_PRFi'_PRFi; byequiv: PRFi'_bad.bad=> //=; 2:smt().
+proc.
+call (: PRFi'_bad.bad
+      , !PRFi'_bad.bad{2} /\ ={PRPi.m} /\ ={PRFi'_bad.bad}
+      , PRFi'_bad.bad{2} /\ ={PRFi'_bad.bad}).
++ exact: D_ll.
++ proc; if=> //=; inline *.
+  seq 1 1: (#pre /\ ={r}); 1:by auto.
+  if {1}; auto=> |> &1 _ x_notin_m _.
+  by apply: excepted_lossless; exists x{1}.
++ move=> &2 bad; proc; if; 2:by auto.
+  seq 1: (PRFi'_bad.bad{2} /\ PRFi'_bad.bad = PRFi'_bad.bad{2} /\ x \notin PRPi.m)=> //.
+  + by auto=> |>; rewrite dD_ll.
+  + if; auto=> |> &1 _ x_notin_m _ @/predT /=.
+    by apply: excepted_lossless; exists x{1}.
+  + by hoare; auto.
+  + by move=> &1; proc; if; auto=> |>; rewrite dD_ll.
+by inline *; auto=> |> /#.
+qed.
+
+import StdBigop.Bigreal BRA.
+
+local lemma pr_PRFi'_bad &m:
+     Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad]
+  <= (q^2 - q)%r / 2%r * hmin_dD.
+proof.
+(** This is easier than instantiating Birthday bound, still **)
+have ->: Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad]
+       = Pr[IND(Count(PRFi'_bad), D).main() @ &m: PRFi'_bad.bad /\ Count.count <= q].
++ byequiv (: ={glob D} ==> ={PRFi'_bad.bad} /\ Count.count{2} <= q)=> //.
+  conseq (: _ ==> ={PRFi'_bad.bad}) _ (: _ ==> Count.count <= q)=> //.
+  + by proc; call (D_count PRFi'_bad 0); inline *; auto.
+  proc; call (: ={PRPi.m, PRFi'_bad.bad})=> //.
+  + by proc; inline *; sp; if; auto.
+  by inline *; auto.
+fel 1 (Count.count) (fun i=> i%r * hmin_dD) q
+    PRFi'_bad.bad
+    [] (card (frng PRPi.m) <= Count.count)=> //.
++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1.
++ by inline *; auto=> |>; rewrite frng0 fcards0.
++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //.
+  proc; inline *; sp; if=> //.
+  + wp; rnd (rng PRPi.m); auto=> |> &0 ge0_count lt_count_q.
+    move=> _ size_rng_m _; rewrite (mu_eq _ _ (mem (frng PRPi.m{0}))).
+    + by move=> x; rewrite mem_frng.
+    apply: (ler_trans ((card (frng PRPi.m{0}))%r * hmin_dD)).
+    + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP.
+    apply: ler_wpmul2r; 1:exact: ge0_hmin_dD.
+    by apply: le_fromint=> /#.
+  by hoare; auto=> |>; smt(ge0_hmin_dD).
++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt().
+  move=> &0 card_rng_m x_notin_m r _; split=> [/#|].
+  have ->: frng PRPi.m.[x <- r]{0} = frng PRPi.m{0} `|` fset1 r.
+  + apply: fsetP=> z; rewrite in_fsetU1 !mem_frng.
+    rewrite rng_set; congr; congr.
+    apply: fmap_eqP=> z0; rewrite remE.
+    case: (z0 = x{0})=> |>.
+    by move: x_notin_m; rewrite domE=> /= ->.
+  by rewrite fcardU1; smt().
+qed.
+
+lemma RP_RF_Switching &m:
+     `|  Pr[IND(PRPi, D).main() @ &m: res]
+       - Pr[IND(PRFi, D).main() @ &m: res]|
+  <= (q ^ 2 - q)%r / 2%r * hmin_dD.
+proof.
+rewrite (pr_PRPi_PRPi'_Direct &m) (pr_PRPi'_Direct_PRPi'_Indirect &m).
+rewrite (pr_PRPi'_Indirect_PRPi'_bad &m).
+smt(pr_PRPi'_Indirect_PRFi pr_PRFi'_bad).
+qed.
+end section.
diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
index 435ecbadcf..735dfe8257 100644
--- a/theories/crypto/prp_prf/Strong_RP_RF.eca
+++ b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -5,55 +5,62 @@ require (*--*) PRP.
 
 require (*--*) FelTactic.
 
-(** We assume a finite domain D, equipped with its uniform
+(** We assume a finite domain D, equipped with a full and lossless
     distribution. **)
 type D.
-op uD: { D distr | is_uniform uD /\ is_lossless uD /\ is_full uD } as uD_uf_fu.
+op [lossless full] dD: D distr.
 
-(** and a type K equipped with a lossless distribution **)
+op hmin_dD: { real | forall d, mu1 dD d <= hmin_dD } as hmin_dDP.
+
+lemma ge0_hmin_dD: 0%r <= hmin_dD.
+proof.
+apply: (ler_trans (mu1 dD witness)).
++ exact: ge0_mu.
+exact: hmin_dDP.
+qed.
+
+(** and a type K **)
 type K.
-op dK: { K distr | is_lossless dK } as dK_ll.
 
 clone import PRP as PRPt with
-  type D  <- D.
+  type D  <- D
+proof *.
 
-clone import StrongPRP as PRPSec.
+clone import StrongPRP as PRPSec
+proof *.
 
 clone import RP as PRPi with
-    op dD <- uD
-proof * by smt(uD_uf_fu)
+    op dD <- dD
+proof *
 rename "RP" as "PRPi".
+realize dD_ll by smt(dD_ll).
 
 (* This is an "Almost (Random Permutation)" (the Almost applies to Permutation) *)
 (* We keep track of collisions explicitly because it's going to be useful anyway *)
 module ARP = {
-  var coll : bool
-  var m, mi: (D,D) fmap
+  var m, mi: (D, D) fmap
 
   proc init(): unit = {
     m    <- empty;
     mi   <- empty;
-    coll <- false;
   }
 
-  proc f(x : D) = {
+  proc f(x: D) = {
     var y;
 
     if (x \notin m) {
-      y      <$ uD;
-      coll   <- coll \/ rng m y;
+      y      <$ dD;
       m.[x]  <- y;
       mi.[y] <- x;
     }
     return oget m.[x];
   }
 
-  proc fi(y : D) = {
+  proc fi(y: D) = {
     var x;
 
     if (y \notin mi) {
-      x      <$ uD;
-      coll   <- coll \/ rng mi x;
+      x      <$ dD;
       m.[x]  <- y;
       mi.[y] <- x;
     }
@@ -61,41 +68,86 @@ module ARP = {
   }
 }.
 
-op q : { int | 0 <= q } as ge0_q.
+module Count (P : PRP) = {
+  var count: int
+
+  proc init() = {
+    P.init();
+    count <- 0;
+  }
+
+  proc f(x) = {
+    var r;
+
+    r <@ P.f(x);
+    count <- count + 1;
+    return r;
+  }
+
+  proc fi(x) = {
+    var r;
+
+    r <@ P.fi(x);
+    count <- count + 1;
+    return r;
+  }
+}.
+
+section.
 
-(** To factor out the difficult step, we parameterize the PRP by a
-    procedure that samples its output, and provide two instantiations
-    of it. **)
-module type Sample_t = {
-  proc sample(X:D -> bool): D
+declare module D <: Distinguisher { -PRPi, -ARP, -Count }.
+declare axiom D_ll (O <: SPRP_Oracles { -D }):
+     islossless O.f
+  => islossless O.fi
+  => islossless D(O).distinguish.
+
+declare op q : { int | 0 <= q } as ge0_q.
+declare axiom D_count (P <: PRP { -D, -Count }) c:
+  hoare [D(Count(P)).distinguish: Count.count = c ==> Count.count <= c + q].
+
+local clone import TwoStepSampling with
+  type i    <- unit,
+  type t    <- D,
+  op   dt _ <- dD
+proof *.
+
+local module type Sample_t = {
+  proc sample(_: D -> bool): D
 }.
 
-module Direct = {
-  proc sample(X:D -> bool): D = {
+local module Direct: Sample_t = {
+  proc sample(X) = {
     var r;
 
-    r <$ uD \ X;
+    r <@ S.direct((), fun _=> X);
     return r;
   }
 }.
 
-module Indirect = {
-  proc sample(X:D -> bool): D = {
+local module Indirect: Sample_t = {
+  proc sample(X) = {
     var r;
 
-    r <$ uD;
-    if (X r) {
-      r <$ uD \ X;
-    }
+    r <@ S.indirect((), fun _=> X);
     return r;
   }
 }.
 
-module PRPi'(S:Sample_t) = {
-  proc init =  PRPi.init
+local equiv eq_Direct_Indirect:
+  Direct.sample ~ Indirect.sample: ={X} ==> ={res}.
+proof. by proc; call ll_direct_indirect_eq; auto; smt(dD_ll). qed.
+
+local module PRPi' (S: Sample_t) = {
+  var bad: bool
+
+  proc init() = {
+    PRPi.init();
+    bad <- false;
+  }
 
   proc f(x:D): D = {
     var r;
+
     if (x \notin PRPi.m) {
       r <@ S.sample(rng PRPi.m);
       PRPi.m.[x] <- r;
@@ -106,6 +158,7 @@ module PRPi'(S:Sample_t) = {
 
   proc fi(x:D): D = {
     var r;
+
     if (x \notin PRPi.mi) {
       r <@ S.sample(rng PRPi.mi);
       PRPi.mi.[x] <- r;
@@ -115,10 +168,76 @@ module PRPi'(S:Sample_t) = {
   }
 }.
 
-(* Some losslessness lemmas *)
-(* FIXME: cleanup *)
+local module ARP_bad = {
+  var bad: bool
+
+  proc init() = {
+    ARP.init();
+    bad <- false;
+  }
+
+  proc f(x) = {
+    var y;
+
+    if (x \notin ARP.m) {
+      y <$ dD;
+      bad <- bad \/ rng ARP.m y;
+      ARP.m.[x] <- y;
+      ARP.mi.[y] <- x;
+    }
+    return oget ARP.m.[x];
+  }
+
+  proc fi(y) = {
+    var x;
+
+    if (y \notin ARP.mi) {
+      x <$ dD;
+      bad <- bad \/ rng ARP.mi x;
+      ARP.m.[x] <- y;
+      ARP.mi.[y] <- x;
+    }
+    return oget ARP.mi.[y];
+  }
+}.
+
+local module PRPi'_bad = {
+  proc init() = {
+    PRPi.init();
+    ARP_bad.bad <- false;
+  }
+
+  proc f(x) = {
+    var y;
+
+    if (x \notin PRPi.m) {
+      y <$ dD;
+      if (rng PRPi.m y) {
+        ARP_bad.bad <- true;
+        y <$ dD \ rng PRPi.m;
+      }
+      PRPi.m.[x] <- y;
+      PRPi.mi.[y] <- x;
+    }
+    return oget PRPi.m.[x];
+  }
+
+  proc fi(y) = {
+    var x;
+
+    if (y \notin PRPi.mi) {
+      x <$ dD;
+      if (rng PRPi.mi x) {
+        ARP_bad.bad <- true;
+        x <$ dD \ rng PRPi.mi;
+      }
+      PRPi.m.[x] <- y;
+      PRPi.mi.[y] <- x;
+    }
+    return oget PRPi.mi.[y];
+  }
+}.
 
-(* FIXME: Duplicate lemmas with RP_RF *)
 lemma notin_supportIP (P : 'a -> bool) (d : 'a distr):
   (exists a, support d a /\ !P a) <=> mu d P < mu d predT.
 proof.
@@ -130,447 +249,181 @@ qed.
 
 lemma excepted_lossless (m:(D,D) fmap):
   (exists x, x \notin m) =>
-  mu (uD \ (rng m)) predT = 1%r.
+  mu (dD \ (rng m)) predT = 1%r.
 proof. 
-move=> /endo_dom_rng [x h]; rewrite dexcepted_ll //.
-+ smt(uD_uf_fu).
-have [?[<- @/is_full Hsupp]]:= uD_uf_fu.
-apply/notin_supportIP;exists x => />;apply Hsupp.
+move=> /endo_dom_rng [x h]; rewrite dexcepted_ll // 1:dD_ll.
+by rewrite -dD_ll; apply: notin_supportIP; exists x; rewrite dD_fu.
 qed.
 
-phoare Indirect_ll: [Indirect.sample: exists x, support uD x /\ !X x ==> true] = 1%r.
+local lemma rng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y:
+  forall z, rng m.[x <- y] z => predU (rng m) (pred1 y) z.
 proof.
-proc; seq  1: (exists x, support uD x /\ !X x)=> //=.
-+ by rnd (predT); skip; smt(uD_uf_fu).
-if=> //=.
-+ rnd (predT); skip.
-  move=> /> &0; rewrite dexceptedE predTI mu_not.
-  move=> x x_in_uD x_notin_X r_in_X.
-  apply/mulrV/ltr0_neq0/subr_gt0/notin_supportIP.
-  by exists x.
-by hoare; rnd=> //=; skip=> &hr ->.
+move=> z; rewrite /predU /pred1 /= (rngE m.[_ <- _])=> /= - [] x0.
+rewrite get_setE; case: (x0 = x)=> |> _ m_x0; left; rewrite rngE /=.
+by exists x0.
 qed.
 
-lemma PRPi'_Indirect_f_ll: islossless PRPi'(Indirect).f.
+local lemma frng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y:
+  frng m.[x <- y] \subset frng m `|` fset1 y.
 proof.
-proc; if=> //=; auto; call Indirect_ll.
-skip=> /> &hr x_notin_m.
-have [x0] x0_notinr_m := endo_dom_rng PRPi.m{hr} _; first by exists x{hr}.
-by exists x0; rewrite x0_notinr_m /=; smt(uD_uf_fu).
+by move=> z; rewrite in_fsetU1 !mem_frng=> /rng_set_subset_rngU1.
 qed.
 
-lemma PRPi'_Indirect_fi_ll: islossless PRPi'(Indirect).fi.
+(** We split this into extremely small steps, but this is not
+    necessary **)
+local lemma pr_PRPi_PRPi'_Direct &m:
+    Pr[IND(PRPi, D).main() @ &m: res]
+  = Pr[IND(PRPi'(Direct), D).main() @ &m:res].
 proof.
-proc; if=> //=; auto; call Indirect_ll.
-skip=> /> &hr x_notin_mi.
-have [x0] x0_notinr_mi := endo_dom_rng PRPi.mi{hr} _; first by exists x{hr}.
-by exists x0; rewrite x0_notinr_mi; smt(uD_uf_fu).
+byequiv=> //; proc; call (: ={glob PRPi}).
++ by proc; if=> //; inline *; auto=> |> &2 _ y _; rewrite get_set_sameE.
++ by proc; if=> //; inline *; auto=> |> &2 _ y _; rewrite get_set_sameE.
+by inline *; auto.
 qed.
 
-(** The proof is cut into 3 parts (sections):
-      - We first focus on proving
-         Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
-         <= Pr[IND(PRFi,D).main() @ &m: res]
-          + Pr[IND(PRFi,D).main() @ &m: collision PRFi.m].
-      - Second, we concretely bound (when the PRF oracle stops
-        answering queries after the q-th):
-          Pr[IND(PRFi,D).main() @ &m: collision PRFi.m]
-          <= q^2 * Pr[x = $uD: x = witness]
-      - We conclude by proving (difficult!)
-         Pr[IND(PRPi,D).main() @ &m: res]
-         = Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
-
-     Purists are then invited to turn the security statement about
-     restricted oracles into a security statement about restricted
-     adversaries. **)
-section Upto.
-  declare module D <: Distinguisher {-PRPi, -ARP}.
-  declare axiom D_ll (O <: SPRP_Oracles {-D}): islossless O.f => islossless O.fi => islossless D(O).distinguish.
-
-  local module PRP_indirect_bad = {
-    var bad : bool
-
-    proc init(): unit = {
-             PRPi.init();
-      bad <- false;
-    }
-
-    proc sample(X:D -> bool): D = {
-      var r;
-
-      r <$ uD;
-      if (X r) {
-        bad <- true;
-        r <$ uD \ X;
-      }
-      return r;
-    }
-
-    proc f(x:D): D = {
-      var r;
-      if (x \notin PRPi.m) {
-        r <@ sample(rng PRPi.m);
-        PRPi.m.[x] <- r;
-        PRPi.mi.[oget PRPi.m.[x]] <- x;
-      }
-      return oget PRPi.m.[x];
-    }
-
-    proc fi(y:D): D = {
-     var r;
-     if (y \notin PRPi.mi) {
-        r <@ sample(rng PRPi.mi);
-        PRPi.mi.[y] <- r;
-        PRPi.m.[oget PRPi.mi.[y]] <- y;
-      }
-      return oget PRPi.mi.[y];
-    }
-  }.
-
-  local lemma PRPi'_Indirect_eq &m:
-    Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
-    = Pr[IND(PRP_indirect_bad,D).main() @ &m: res].
-  proof. by byequiv=> //=; proc; inline *; sim. qed.
-
-  (** Upto failure: if a collision does not occur in PRFi.m, then the
-      programs are equivalent **)
-  lemma pr_PRPi'_Indirect_ARP &m:
-    `|Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
-      - Pr[IND(ARP,D).main() @ &m: res]|
-    <= Pr[IND(ARP,D).main() @ &m: ARP.coll].
-  proof.
-  rewrite (PRPi'_Indirect_eq &m).
-  byequiv: PRP_indirect_bad.bad=> //=; 2:smt().
-  proc.
-  call (_: ARP.coll,
-             !PRP_indirect_bad.bad{1} /\ ={m,mi}(PRPi,ARP),
-             (PRP_indirect_bad.bad{1} <=> ARP.coll{2})).
-  + exact D_ll.
-  + proc. if=> //=; inline *.
-    swap{1} 1.
-    seq  1  4: (={x} /\
-                x{1} \notin PRPi.m{1} /\
-                ARP.m{2} = PRPi.m.[x <- r0]{1} /\
-                ARP.mi{2} = PRPi.mi.[r0 <- x]{1} /\
-                ((PRP_indirect_bad.bad \/ rng PRPi.m r0){1} <=> ARP.coll{2})).
-      by auto=> /#.
-    sp; if{1}.
-      conseq (_: PRP_indirect_bad.bad{1} /\ ARP.coll{2})=> //=.
-      auto; progress [-split]; split=> //= [|_].
-        by apply/excepted_lossless => /#.
-      by progress; right.
-    by auto; progress [-split]; rewrite H0 /= => -> /=; rewrite get_setE.
-  + move=> &2 bad; conseq (_: true ==> true: =1%r)
-                          (_: PRP_indirect_bad.bad ==> PRP_indirect_bad.bad)=> //=.
-      by proc; if=> //=; inline *; seq  2: PRP_indirect_bad.bad; [auto|if=> //=; auto].
-    proc; if=> //=; inline *.
-    seq  2: (X = rng PRPi.m /\ x \notin PRPi.m) 1%r 1%r 0%r _ => //=.
-      by auto; rewrite -/predT; smt(uD_uf_fu).
-      by if=> //=; auto=> /> *; apply/excepted_lossless => /#.
-      by hoare; auto.
-  + move=> &1.
-    proc; if; auto; progress [-split]; rewrite -/predT; split=> //= [|_]; 1:smt(uD_uf_fu).
-    by progress [-split]; rewrite H.
-  + proc. if=> //=; inline *.
-    swap{1} 1.
-    seq  1  4: (={y} /\
-                y{1} \notin PRPi.mi{1} /\
-                ARP.m{2} = PRPi.m.[r0 <- y]{1} /\
-                ARP.mi{2} = PRPi.mi.[y <- r0]{1} /\
-                ((PRP_indirect_bad.bad \/ rng PRPi.mi r0){1} <=> ARP.coll{2})).
-      by auto=> /#.
-    sp; if{1}.
-      conseq (_: PRP_indirect_bad.bad{1} /\ ARP.coll{2})=> //=.
-      auto; progress [-split]; split=> //= [|_].
-        by apply/excepted_lossless => /#.
-      by progress; right.
-    by auto; progress [-split]; rewrite H0 => /= ->; rewrite get_setE.
-  + move=> &2 bad; conseq (_: true ==> true: =1%r)
-                          (_: PRP_indirect_bad.bad ==> PRP_indirect_bad.bad)=> //=.
-      by proc; if=> //=; inline *; seq  2: PRP_indirect_bad.bad; [auto|if=> //=; auto].
-    proc; if=> //=; inline *.
-    seq  2: (X = rng PRPi.mi /\ y \notin PRPi.mi) 1%r 1%r 0%r _ => //=.
-      by auto; rewrite -/predT; smt(uD_uf_fu).
-      by if=> //=; auto=> /> *; apply/excepted_lossless => /#.
-      by hoare; auto.
-  + move=> &1.
-    proc; if; auto; progress [-split]; rewrite -/predT; split=> //= [|_]; 1:smt(uD_uf_fu).
-    by progress [-split]; rewrite H.
-  by inline *; auto; progress => /#.
-  qed.
-end section Upto.
-
-(** We now bound the probability of collisions. We cannot do so
-    by instantiating the generic Birthday Bound result. It's still
-    the Birthday Bound, though, just not generic:
-      Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll]
-      <= q^2 * Pr[x = $uD: x = witness],
-
-    where DBounder prevents the distinguisher from calling the
-    f-oracle more than q times. **)
-module DBounder (D : Distinguisher) (F : SPRP_Oracles) = {
-  module FBounder = {
-    var c:int
-
-    proc f(x:D): D = {
-      var r <- witness;
-
-      if (c < q) {
-        r <@ F.f(x);
-        c <- c + 1;
-      }
-      return r;
-    }
-
-    proc fi(x:D): D = {
-      var r <- witness;
-
-      if (c < q) {
-        r <@ F.fi(x);
-        c <- c + 1;
-      }
-      return r;
-    }
-  }
-
-  proc distinguish(): bool = {
-    var b;
-
-    FBounder.c <- 0;
-    b          <@ D(FBounder).distinguish();
-    return b;
-  }
-}.
-
-section CollisionProbability.
-  require import Mu_mem.
-  (*---*) import StdBigop StdRing StdOrder.
-  (*---*) import Bigreal.BRA RField RField.AddMonoid IntOrder.
-
-  declare module D <: Distinguisher {-ARP, -DBounder}.
-  declare axiom D_ll (O <: SPRP_Oracles {-D}): islossless O.f => islossless O.fi => islossless D(O).distinguish.
-
-  local module FEL (D : Distinguisher) = {
-    var c : int
-
-    module FBounder = {
-      proc f(x:D): D = {
-        var r <- witness;
+local lemma pr_PRPi'_Direct_PRPi'_Indirect &m:
+    Pr[IND(PRPi'(Direct), D).main() @ &m: res]
+  = Pr[IND(PRPi'(Indirect), D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={glob PRPi}).
++ proc; if=> //; auto.
+  by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll.
++ proc; if=> //; auto.
+  by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll.
+by inline *; auto.
+qed.
 
-        if (c < q) {
-          if (card (frng ARP.m) < q) {
-            r <@ ARP.f(x);
-          }
-          c <- c + 1;
-        }
-        return r;
-      }
+local lemma pr_PRPi'_Indirect_PRPi'_bad &m:
+    Pr[IND(PRPi'(Indirect), D).main() @ &m: res]
+  = Pr[IND(PRPi'_bad, D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={glob PRPi}).
++ proc; if=> //; inline *.
+  do ! cfold {1} 1.
+  seq 1 1: (#pre /\ r1{1} = y{2}); 1:by auto.
+  if=> //; auto=> |>.
+  + by move=> &2 _ _ y _; rewrite get_set_sameE.
+  by move=> &2; rewrite get_set_sameE.
++ proc; if=> //; inline *.
+  do ! cfold {1} 1.
+  seq 1 1: (#pre /\ r1{1} = x{2}); 1:by auto.
+  if=> //; auto=> |>.
+  + by move=> &2 _ _ y _; rewrite get_set_sameE.
+  by move=> &2; rewrite get_set_sameE.
+by inline *; auto.
+qed.
 
-      proc fi(x:D): D = {
-        var r <- witness;
+local lemma pr_ARP_ARP_bad &m:
+    Pr[IND(ARP, D).main() @ &m: res]
+  = Pr[IND(ARP_bad, D).main() @ &m: res].
+proof.
+byequiv=> //; proc; call (: ={glob ARP}); 1,2:by sim.
+by inline *; auto.
+qed.
 
-        if (c < q) {
-          if (card (frng ARP.mi) < q) {
-            r <@ ARP.fi(x);
-          }
-          c <- c + 1;
-        }
-        return r;
-      }
-    }
+local lemma pr_PRP_bad_ARP_bad &m:
+     `|  Pr[IND(PRPi'_bad, D).main() @ &m: res]
+       - Pr[IND(ARP, D).main() @ &m: res]|
+  <= Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad].
+proof.
+rewrite pr_ARP_ARP_bad; byequiv: ARP_bad.bad=> //=; 2:smt().
+proc.
+call (: ARP_bad.bad
+      , !ARP_bad.bad{2} /\ ={m, mi}(PRPi, ARP) /\ ={ARP_bad.bad}
+      , ARP_bad.bad{2} /\ ={ARP_bad.bad}).
++ exact: D_ll.
++ proc; if=> //=; inline *.
+  seq 1 1: (#pre /\ ={y}); 1:by auto.
+  if {1}; auto=> |> &1 _ x_notin_m _.
+  by apply: excepted_lossless; exists x{1}.
++ move=> &2 bad; proc; if; 2:by auto.
+  seq 1: (ARP_bad.bad{2} /\ ARP_bad.bad = ARP_bad.bad{2} /\ x \notin PRPi.m)=> //.
+  + by auto=> |>; rewrite dD_ll.
+  + if; auto=> |> &1 _ x_notin_m _ @/predT /=.
+    by apply: excepted_lossless; exists x{1}.
+  + by hoare; auto.
+  + by move=> &1; proc; if; auto=> |>; rewrite dD_ll.
++ proc; if=> //=; inline *.
+  seq 1 1: (#pre /\ ={x}); 1:by auto.
+  if {1}; auto=> |> &1 _ y_notin_m _.
+  by apply: excepted_lossless; exists y{1}.
++ move=> &2 bad; proc; if; 2:by auto.
+  seq 1: #pre=> //.
+  + by auto=> |>; rewrite dD_ll.
+  + if; auto=> |> &1 _ x_notin_m _ @/predT /=.
+    by apply: excepted_lossless; exists y{1}.
+  + by hoare; auto.
+  + by move=> &1; proc; if; auto=> |>; rewrite dD_ll.
+by inline *; auto=> |> /#.
+qed.
 
-    proc main(): bool = {
-      var b : bool;
+import StdBigop.Bigreal BRA.
 
-           ARP.init();
-      c <- 0;
-      b <@ D(FBounder).distinguish();
-      return b;
-    }
-  }.
-
-  lemma pr_PRFi_collision &m:
-    Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll]
-    <= (q^2 - q)%r / 2%r * mu uD (pred1 witness).
-  proof.
-  have ->: Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll]
-           = Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll /\ DBounder.FBounder.c <= q].
-  + byequiv=> //=; conseq (_: ={glob D} ==> ={ARP.coll,DBounder.FBounder.c})
-                          (_: true ==> DBounder.FBounder.c <= q)=> //=.
-    * proc; inline *; wp; call (_: DBounder.FBounder.c <= q).
-      - by proc; sp; if=> //=; inline*; sp; if=> //=; auto=> /#.
-      - by proc; sp; if=> //=; inline*; sp; if=> //=; auto=> /#.
-      by auto=> /=; apply/ge0_q.
-    by sim.
-  have ->: Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll /\ DBounder.FBounder.c <= q]
-           = Pr[FEL(D).main() @ &m: ARP.coll /\ FEL.c <= q].
-  + byequiv=> //=; proc; inline *; wp.
-    call (_: ={glob ARP} /\ ={c}(DBounder.FBounder,FEL) /\ card (frng ARP.m){1} <= FEL.c{2} /\ card (frng ARP.mi){1} <= FEL.c{2}).
-    * proc; sp; if=> //=. rcondt{2} 1; first by auto=> /#.
-      inline *; sp; if=> //=; auto => [/>|/>/#].
-      progress.
-      - apply/(ler_trans (card (frng ARP.m{2} `|` fset1 yL))).
-        + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0].
-          rewrite get_setE; case: (x0 = x{2})=> [<<- /= ->|_ mx0] //.
-          by left; exists x0.
-        by rewrite fcardU fcard1; smt(fcard_ge0).
-      - apply/(ler_trans (card (frng ARP.mi{2} `|` fset1 x{2}))).
-        + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0].
-          rewrite get_setE; case: (x0 = yL)=> [<<- //|_ mx0].
-          by left; exists x0.
-        by rewrite fcardU fcard1; smt(fcard_ge0).
-    * proc; sp; if=> //=. rcondt{2} 1; first by auto=> /#.
-      inline *; sp; if=> //=; auto  => [/>|/>/#].
-      progress.
-      - apply/(ler_trans (card (frng ARP.m{2} `|` fset1 x{2}))).
-        + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0].
-          rewrite get_setE; case: (x0 = x0L)=> [<<- //|_ mx0].
-          by left; exists x0.
-        by rewrite fcardU fcard1; smt(fcard_ge0).
-      - apply/(ler_trans (card (frng ARP.mi{2} `|` fset1 x0L))).
-        + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0].
-          rewrite get_setE; case: (x0 = x{2})=> [<<- //|_ mx0].
-          by left; exists x0.
-        by rewrite fcardU fcard1; smt(fcard_ge0).
-    by auto=> />; rewrite frng0 fcards0.
-  fel 2 FEL.c (fun x, x%r * mu uD (pred1 witness)) q (ARP.coll) 
-           [FEL(D).FBounder.f: (FEL.c < q); FEL(D).FBounder.fi: (FEL.c < q)]
-           (card (fdom ARP.m) <= FEL.c /\ card (fdom ARP.mi) <= FEL.c)=> //.
-  + rewrite -mulr_suml Bigreal.sumidE 1:ge0_q. 
-    by rewrite expr2;smt(mu_bounded ge0_q).
-  + by inline*; auto=> />; rewrite fdom0 fcards0.
-  + exists*FEL.c;elim*=> c.
-    conseq(:_==>_ : (c%r * mu1 uD witness))=> />.
-    proc; sp; rcondt 1=> //.
-    inline *; sp; if=> //=; last first.
-    * hoare; auto=> // /> &hr 6?.
-      by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q).
-    sp; if=> //=.
-    * wp; rnd (rng ARP.m); skip.
-      progress.
-      - apply/(RealOrder.ler_trans ((card (frng ARP.m{hr}))%r * mu uD (pred1 witness))).
-        have ->: rng ARP.m{hr} = mem (frng ARP.m{hr}).
-        + by apply/fun_ext=> x; rewrite mem_frng.
-        apply/mu_mem_le; move=> x _; have [] uD_suf [] ? uD_fu:= uD_uf_fu.
-        apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //.
-        by apply/RealOrder.ler_wpmul2r; smt(mu_bounded lt_fromint ltrW leq_card_rng_dom).
-      - by move: H9;rewrite H1.
-    * by hoare; auto=> //=; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
-  + move=> c; proc. rcondt 2; 1:by auto.
-    sp; if=> //=.
-    * inline*;sp;if;auto; 2:smt().
-      move=> &hr /> + + + + + y />.
-      by rewrite !fdom_set !fcardU !fcard1; smt(fcard_ge0).
-    * by auto=> /#.
-  + by move=> b c; proc; rcondf 2; auto.
-  + exists*FEL.c;elim*=> c.
-    conseq(:_==>_ : (c%r * mu1 uD witness));progress.
-    proc; sp; rcondt 1=> //=.
-    inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
-    sp; if=> //=.
-    * wp; rnd (rng ARP.mi); skip.
-      progress.
-      - apply/(RealOrder.ler_trans ((card (frng ARP.mi{hr}))%r * mu uD (pred1 witness))).
-        have ->: rng ARP.mi{hr} = mem (frng ARP.mi{hr}).
-        + by apply/fun_ext=> x; rewrite mem_frng.
-        apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu.
-        apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //.
-        apply: RealOrder.ler_wpmul2r.
-        + exact: ge0_mu.
-        + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)).
-      - by move: H9; rewrite H1.
-    * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
-  + move=> c; proc; rcondt 2; 1:by auto.
-    sp; if=> //=.
-    * inline*;sp;if;auto; 2:smt().
-      move=> &hr /> + + + + + x.
-      by rewrite !fdom_set !fcardU !fcard1; smt(fcard_ge0).
-    * by auto=> /#.
-  + by move=> b c; proc; rcondf 2; auto.
-  qed.
-end section CollisionProbability.
-
-(* We pull together the results of the first two sections *)
-lemma PartialConclusion (D <: Distinguisher {-PRPi, -ARP, -DBounder}) &m:
-  (forall (O <: SPRP_Oracles {-D}), islossless O.f => islossless O.fi => islossless D(O).distinguish) =>
-  `|Pr[IND(PRPi'(Indirect),DBounder(D)).main() @ &m: res]
-    - Pr[IND(ARP,DBounder(D)).main() @ &m: res]|
-  <= (q^2 - q)%r / 2%r * mu uD (pred1 witness).
+local lemma pr_ARP_bad &m:
+     Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad]
+  <= (q^2 - q)%r / 2%r * hmin_dD.
 proof.
-move=> D_ll.
-have:= pr_PRFi_collision D D_ll &m.
-have /#:= pr_PRPi'_Indirect_ARP (DBounder(D)) _ &m.
-move=> O O_f_ll O_fi_ll; proc.
-call (D_ll (<: DBounder(D,O).FBounder) _ _).
-  by proc; sp; if=> //=; wp; call O_f_ll.
-  by proc; sp; if=> //=; wp; call O_fi_ll.
-by auto.
+have ->: Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad]
+       = Pr[IND(Count(ARP_bad), D).main() @ &m: ARP_bad.bad /\ Count.count <= q].
++ byequiv (: ={glob D} ==> ={ARP_bad.bad} /\ Count.count{2} <= q)=> //.
+  conseq (: _ ==> ={ARP_bad.bad}) _ (: _ ==> Count.count <= q)=> //.
+  + by proc; call (D_count ARP_bad 0); inline *; auto.
+  proc; call (: ={ARP.m, ARP.mi, ARP_bad.bad})=> //.
+  + by proc; inline *; sp; if; auto=> |>.
+  + by proc; inline *; sp; if; auto.
+  by inline *; auto.
+fel 1 (Count.count) (fun i=> i%r * hmin_dD) q
+    ARP_bad.bad
+    [] (card (frng ARP.m) <= Count.count /\ card (frng ARP.mi) <= Count.count)=> //.
++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1.
++ by inline *; auto=> |>; rewrite frng0 fcards0.
++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //.
+  proc; inline *; sp; if=> //.
+  + wp; rnd (rng ARP.m); auto=> |> &0 ge0_count lt_count_q.
+    move=> _ size_rng_m _ _; rewrite (mu_eq _ _ (mem (frng ARP.m{0}))).
+    + by move=> x; rewrite mem_frng.
+    apply: (ler_trans ((card (frng ARP.m{0}))%r * hmin_dD)).
+    + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP.
+    apply: ler_wpmul2r; 1:exact: ge0_hmin_dD.
+    by apply: le_fromint=> /#.
+  by hoare; auto=> |>; smt(ge0_hmin_dD).
++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt().
+  move=> &0 card_rng_m card_rng_mi x_notin_m r _; split=> [/#|].
+  split.
+  + apply: (lez_trans (card (frng ARP.m{0} `|` fset1 r))).
+    + exact/subset_leq_fcard/frng_set_subset_rngU1.
+    by rewrite fcardU1 /#.
+  apply: (lez_trans (card (frng ARP.mi{0} `|` fset1 x{0}))).
+  + exact/subset_leq_fcard/frng_set_subset_rngU1.
+  by rewrite fcardU1 /#.
++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //.
+  proc; inline *; sp; if=> //.
+  + wp; rnd (rng ARP.mi); auto=> |> &0 ge0_count lt_count_q.
+    move=> _ _ size_rng_mi _; rewrite (mu_eq _ _ (mem (frng ARP.mi{0}))).
+    + by move=> x; rewrite mem_frng.
+    apply: (ler_trans ((card (frng ARP.mi{0}))%r * hmin_dD)).
+    + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP.
+    apply: ler_wpmul2r; 1:exact: ge0_hmin_dD.
+    by apply: le_fromint=> /#.
+  by hoare; auto=> |>; smt(ge0_hmin_dD).
++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt().
+  move=> &0 card_rng_m card_rng_mi x_notin_m r _; split=> [/#|].
+  split.
+  + apply: (lez_trans (card (frng ARP.m{0} `|` fset1 x{0}))).
+    + exact/subset_leq_fcard/frng_set_subset_rngU1.
+    by rewrite fcardU1 /#.
+  apply: (lez_trans (card (frng ARP.mi{0} `|` fset1 r))).
+  + exact/subset_leq_fcard/frng_set_subset_rngU1.
+  by rewrite fcardU1 /#.
 qed.
 
-(** This section proves the equivalence between the Ideal PRP and the
-    module PRPi'(Indirect) used in section Upto. **)
-section PRPi_PRPi'_Indirect.
-  local clone include Dexcepted.TwoStepSampling with
-    type i    <- unit,
-    type t    <- D,
-    op   dt _ <- uD
-  proof *.
-
-  (* The key is in proving that Direct.sample and Indirect.sample
-     define the same distribution. We do this by extensional equality
-     of distributions:
-       forall a, Pr[Direct.sample: res = a] = Pr[Indirect.sample: res = a]. *)
-  equiv eq_Direct_Indirect: Direct.sample ~ Indirect.sample: ={X} ==> ={res}.
-  proof.
-  proc.
-  outline {1} 1 by { r <@ S.direct((), fun _ => X); }.
-  rewrite equiv[{1} 1 ll_direct_indirect_eq ((), fun _ => X :@ r)].
-  + auto=> />; exact dD_ll.
-  inline S.indirect.
-  by sp; seq 1 1 : (#pre /\ r0{1} = r{2}); auto; if; auto.
-  qed.
-
-  (* The rest is easy *)
-  local equiv eq_PRPi_PRPi'_f_Indirect: PRPi.f ~ PRPi'(Indirect).f:
-    ={x, PRPi.m, PRPi.mi} ==> ={res, PRPi.m, PRPi.mi}.
-  proof.
-  transitivity PRPi'(Direct).f (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}) (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}).
-  + by move=> &1 &2 [->> [->> ->>]]; exists PRPi.m{2} PRPi.mi{2} x{2}.
-  + done.
-  + by proc; inline *; if=> //=; auto; progress; rewrite get_setE.
-  + by proc; if=> //=; wp; call eq_Direct_Indirect.
-  qed.
-
-  local equiv eq_PRPi_PRPi'_fi_Indirect: PRPi.fi ~ PRPi'(Indirect).fi:
-    y{1} = x{2} /\ ={PRPi.m, PRPi.mi} ==> ={res, PRPi.m, PRPi.mi}.
-  proof.
-  transitivity PRPi'(Direct).fi (={PRPi.m,PRPi.mi} /\ y{1} = x{2} ==> ={PRPi.m,PRPi.mi,res}) (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}).
-  + by move=> &1 &2 [->> [->> ->>]]; exists PRPi.m{2} PRPi.mi{2} x{2}.
-  + done.
-  + by proc; inline *; if=> //=; auto; progress; rewrite get_setE.
-  + by proc; if=> //=; wp; call eq_Direct_Indirect.
-  qed.
-
-  declare module D <: Distinguisher {-PRPi}.
-
-  lemma pr_PRPi_PRPi'_Indirect &m:
-    Pr[IND(PRPi,D).main() @ &m: res] = Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
-  proof.
-  byequiv=> //=.
-  proc.
-  call (_: ={PRPi.m,PRPi.mi}).
-    by apply eq_PRPi_PRPi'_f_Indirect.
-    by apply eq_PRPi_PRPi'_fi_Indirect.
-  by inline*; auto.
-  qed.
-end section PRPi_PRPi'_Indirect.
-
-lemma Conclusion (D <: Distinguisher {-PRPi, -ARP, -DBounder}) &m:
-  (forall (O <: SPRP_Oracles {-D}), islossless O.f => islossless O.fi => islossless D(O).distinguish) =>
-  `|Pr[IND(PRPi,DBounder(D)).main() @ &m: res]
-    - Pr[IND(ARP,DBounder(D)).main() @ &m: res]|
-  <= (q^2 - q)%r / 2%r * mu uD (pred1 witness).
+lemma Strong_RP_RF_Switching &m:
+     `|  Pr[IND(PRPi, D).main() @ &m: res]
+       - Pr[IND(ARP, D).main() @ &m: res]|
+  <= (q ^ 2 - q)%r / 2%r * hmin_dD.
 proof.
-move=> D_ll.
-by rewrite (pr_PRPi_PRPi'_Indirect (DBounder(D)) &m) (PartialConclusion D &m D_ll).
+rewrite (pr_PRPi_PRPi'_Direct &m) (pr_PRPi'_Direct_PRPi'_Indirect &m).
+rewrite (pr_PRPi'_Indirect_PRPi'_bad &m).
+smt(pr_PRP_bad_ARP_bad pr_ARP_bad).
 qed.
+end section.