diff --git a/proof/security/FO_TT.ec b/proof/security/FO_TT.ec
index cb1f7f80..b2deba5f 100644
--- a/proof/security/FO_TT.ec
+++ b/proof/security/FO_TT.ec
@@ -67,8 +67,6 @@ op [lossless] randd : randomness distr.
 
 clone import PKE_ROM.PKE as PKE with
   type plaintext <- plaintext,
-  type OWvsIND_RO.RO.out_t <- randomness,
-  op OWvsIND_RO.RO.dout <- fun _ => randd,
   op dplaintext <- dplaintext,
   op MFinT.enum <- FinT.enum
   proof MFinT.enum_spec by apply FinT.enum_spec
@@ -807,44 +805,10 @@ module AdvOW_query (A:PCVA_ADV) = {
 (**** MODULES REQUIRED FOR TIGHT IND-CPA***************)
 (******************************************************)
 
-
-module O_AdvOW_MERGE = {
-  var pk : pkey
-  proc pco(m : plaintext, c : ciphertext) : bool = {
-    var r, c';
-    r  <@ OWvsIND_RO.RO.RO.get(m);
-    c' <- enc r pk m;
-    return c = c';
-  }
-  
-  proc cvo(c:ciphertext) : bool = {
-    var rv; 
-    rv <- false; 
-    if (c <> OW_PCVA.cc) 
-      rv <- find (fun m r => c = enc r pk m) OWvsIND_RO.RO.RO.m <> None;
-    return rv;
-  }
-}.
-
-module AdvOW_query_MERGE (A:PCVA_ADV) = {
-  import var OW_PCVA O_AdvOW_MERGE
-
-  module A = A(CountH(OWvsIND_RO.RO.RO), CountO(O_AdvOW_MERGE))
-
-  proc main(pk0:pkey, c:ciphertext) : unit = {
-    var m' : plaintext option;
-    pk <- pk0; 
-    OWvsIND_RO.RO.RO.init();
-    cc       <- c; 
-    CountO(O_AdvOW_MERGE).init();
-    m'       <@ A.find(pk,cc);
-  }
-
-  proc find(pk0:pkey, c:ciphertext) : plaintext option = {
-    var i : int;
-    main(pk0, c);
-    i        <$ [0 .. qH + qP - 1];
-    return Some (nth witness (elems (fdom OWvsIND_RO.RO.RO.m)) i);
+module AdvOWL_query (A:PCVA_ADV) = {
+  proc find(pk0:pkey, c:ciphertext) : plaintext list = {
+       AdvOW_query(A).find(pk0,c);
+       return elems (fdom RO.RO.m);
   }
 }.
 
@@ -853,10 +817,8 @@ module AdvOW_query_MERGE (A:PCVA_ADV) = {
 (******************************************************)
 
 section. 
-
-declare module A <: PCVA_ADV { -RO.RO, -OW_PCVA, -RO.RO, -RO.FRO, -OW_CPA,
-               -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B, -BOWp, -OWvsIND.Bow,
-               - OWvsIND_RO.RO.RO, -AdvOW_query_MERGE, -OWvsIND_RO.RO.RO.m}.
+declare module A <: PCVA_ADV { -RO.RO, -OW_PCVA, -RO.RO, -RO.FRO, -OW_CPA, -OWL_CPA,
+               -CountO, -Gm, -O_AdvOW, -Correctness_Adv1, -B, -BOWp, -OWvsIND.Bowl}.
 
 local module PCO(RO:RO.RO) = {
   import var OW_PCVA
@@ -2003,7 +1965,7 @@ local lemma G3_CPA_query &m :
 
   Pr[G3.main() @ &m : dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m /\ Gm.m \in RO.RO.m] <=
      2%r * ((qH + qP)%r * eps_msg + 
-        `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r |).
+        `| Pr[PKE.CPA(BasePKE,OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r |).
 proof.
 move => A_count All.
 case (qH = 0 /\ qP = 0). 
@@ -2019,23 +1981,39 @@ case (qH = 0 /\ qP = 0).
 move => *.
   have : Pr[G3.main() @ &m :Gm.m \in RO.RO.m] <=
      2%r * ((qH + qP)%r * eps_msg + 
-        `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r |); last
+        `| Pr[PKE.CPA(BasePKE,OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r |); last
       by rewrite Pr[mu_split dec OW_PCVA.sk.`2 OW_PCVA.cc = Some Gm.m]; smt(mu_bounded).
-  (* PROBLEM INSTANTIATING: THIS PROOF WILL NEED TO BE DONE HERE UNLESS I CAN FIND A SOLUTION 
-     TO THE MODULE RESTRICTIONS.
-  have := OWvsIND_RO.ow_ind_ro BasePKE (AdvOW_query_MERGE(A)) &m _ _ _ _;1..3:by islossless.
-  +  (* lossless *) *)
-  have  : Pr[OW_CPA(BasePKE, AdvOW_query_MERGE(A)).main() @ &m : OW_CPA.m \in OWvsIND_RO.RO.RO.m] <=
-    2%r * ((qH + qP)%r * eps_msg + `|Pr[PKE.CPA(BasePKE, OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r / 2%r|) by admit. (* this goes away if instantiation possible *)
-  have  -> : Pr[OW_CPA(BasePKE, AdvOW_query_MERGE(A)).main() @ &m : OW_CPA.m \in OWvsIND_RO.RO.RO.m] =
+  have := OWvsIND.ow_ind_l BasePKE (AdvOWL_query(A)) &m (qH + qP) _ _ _ _ _ _;2..4:by islossless.
+  + by smt(ge0_qH ge0_qP).
+  + islossless; 1: by apply (All (CountH(RO.RO)) (CountO(O_AdvOW))); islossless.
+    by smt(drange_ll ge0_qH ge0_qP).
+  + proc;inline *;rnd;conseq (:_ ==> card (fdom RO.RO.m) <= qH + qP); 1: by smt().
+    call(: card (fdom RO.RO.m) = 0 /\ CountO.c_h = 0 /\ CountO.c_cvo = 0 /\ CountO.c_pco = 0 ==> 
+           CountO.c_h <= qH /\ CountO.c_cvo <= qV /\ CountO.c_pco <= qP /\
+           (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco)).
+      conseq (: CountO.c_h =0 /\ CountO.c_pco = 0 /\
+           (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco) ==> 
+               
+           (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco))
+         (A_count (<:RO.RO) (<:O_AdvOW)) => />; 1: by smt().
+  proc (
+         (card (fdom RO.RO.m) <= CountO.c_h + CountO.c_pco)) => //. 
+  + by proc;inline *;auto.
+  + by proc;inline *;auto;smt(fdom_set fcardU fcard1 fcard_ge0). 
+  + by proc;inline *;auto;smt(fdom_set fcardU fcard1 fcard_ge0). 
+  by auto => />;smt(fcards0 fdom0).
+
+  have  -> : Pr[OWL_CPA(BasePKE, AdvOWL_query(A)).main() @ &m : OWL_CPA.m \in OWL_CPA.l] =
              Pr[G3.main() @ &m : Gm.m \in RO.RO.m]; last by done.
   
-  byequiv (_: _ ==> OWvsIND_RO.RO.RO.m{1} = RO.RO.m{2} /\ OW_CPA.m{1} = Gm.m{2} /\ O_AdvOW_MERGE.pk{1} = O_AdvOW.pk{2}) => //.
-  proc;inline *;wp;rnd{1};call(_: ={OW_PCVA.cc} /\ OWvsIND_RO.RO.RO.m{1} = RO.RO.m{2} /\ OW_CPA.m{1} = Gm.m{2} /\ O_AdvOW_MERGE.pk{1} = O_AdvOW.pk{2}).
+  byequiv => //.
+  proc;inline *;wp;rnd{1}; conseq (:_ ==> OWL_CPA.m{1} = Gm.m{2} /\ ={RO.RO.m}); 
+    1: by smt(mem_fdom drange_ll ge0_qH ge0_qP).
+  call(_: ={OW_PCVA.cc, RO.RO.m} /\ OWL_CPA.m{1} = Gm.m{2} /\ O_AdvOW.pk{1} = O_AdvOW.pk{2}).
   + by sim.
   + by sim.
   + by sim.
-  by auto => />;smt(drange_ll ge0_qH ge0_qP).
+  by auto => />.
 qed.
 
 lemma pre_conclusion_cpa &m gamma_spread :
@@ -2050,9 +2028,9 @@ lemma pre_conclusion_cpa &m gamma_spread :
   islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) =>
 
   Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <=
-      2%r * `|Pr[PKE.CPA(BasePKE, OWvsIND.Bow(AdvOW(A))).main() @ &m : res] - 1%r / 2%r| 
-    + 2%r * `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r | 
-    + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query_MERGE(A))).main() @ &m : res ]
+      2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| 
+    + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | 
+    + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ]
     + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res]
     + Pr[ Correctness_Adv(RO.RO,TT,AdvCorr(A)).main() @ &m : res ]
     + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg.
@@ -2086,9 +2064,9 @@ lemma conclusion_cpa &m gamma_spread :
   islossless O.cvo => islossless O.pco => islossless H0.get => islossless A(H0, O).find) =>
 
   Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <=
-      2%r * `|Pr[PKE.CPA(BasePKE, OWvsIND.Bow(AdvOW(A))).main() @ &m : res] - 1%r / 2%r| 
-    + 2%r * `| Pr[PKE.CPA(BasePKE,OWvsIND_RO.BowROM(AdvOW_query_MERGE(A))).main() @ &m : res] - 1%r/2%r | 
-    + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query_MERGE(A))).main() @ &m : res ]
+      2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| 
+    + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | 
+    + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ]
     + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res]
     + (qH + qP + 2)%r * Pr[ PKE.Correctness_Adv(BasePKE,B(AdvCorr(A),RO.RO)).main() @ &m : res ]
     + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg.
@@ -2110,7 +2088,5 @@ proof.
   by smt().
 qed.
 
-
-
 end section.
 
diff --git a/proof/security/FO_UU.ec b/proof/security/FO_UU.ec
index 04075461..15f48713 100644
--- a/proof/security/FO_UU.ec
+++ b/proof/security/FO_UU.ec
@@ -1313,48 +1313,15 @@ qed.
 
 (* Instantiation *)
 
-(* lemma correctness:
-  forall (A0(H0 : PKEROM.POracle) <:
-           PKEROM.CORR_ADV{+all mem, -PKEROM.RO.RO, -PKEROM.RO.FRO, -Correctness_Adv1, -B} [find : {H0.get} ]) &m,
-    qHC < FinT.card - 1 =>
-    (forall (RO <: PKEROM.RO.RO{+all mem, -CO1, -A0} ),
-       hoare[ Correctness_Adv1(RO, A0).A.find : CO1.counter = 0 ==> CO1.counter <= qHC]) =>
-    (forall (H0 <: PKEROM.POracle{+all mem, -A0} ), islossless H0.get => islossless A0(H0).find) =>
-    Pr[PKEROM.Correctness_Adv(PKEROM.RO.RO, TT, A0).main() @ &m : res] <=
-    (qHC + 1)%r * Pr[Correctness_Adv(BasePKE, B(A0, PKEROM.RO.RO)).main() @ &m : res]. *)
-
 (* 
-lemma conclusion:
-  forall (A0(H0 : PKEROM.POracle, O : PKEROM.VA_ORC) <:
-           PKEROM.PCVA_ADV{+all mem, -PKEROM.RO.RO, -PKEROM.RO.FRO, -PKEROM.OW_PCVA, -Correctness_Adv1, -B, -CountO, -O_AdvOW, -Gm}
-             [find : {O.cvo, O.pco, H0.get} ]) &m (gamma_spread : real),
-    qH + qP + 1 = qHC =>
-    qHC < FinT.card - 1 =>
-    gamma_spread_ok gamma_spread =>
-    (forall (RO <: PKEROM.POracle{+all mem, -CountO, -A0} ) (O <: PKEROM.VA_ORC{+all mem, -CountO, -A0} ),
-       hoare[ A0(CountH(RO), CountO(O)).find :
-               CountO.c_h = 0 /\ CountO.c_cvo = 0 /\ CountO.c_pco = 0 ==>
-               CountO.c_h <= qH /\ CountO.c_cvo <= qV /\ CountO.c_pco <= qP]) =>
-    (forall (H0 <: PKEROM.POracle{+all mem, -A0} ) (O <: PKEROM.VA_ORC{+all mem, -A0} ),
-       islossless O.cvo => islossless O.pco => islossless H0.get => islossless A0(H0, O).find) =>
-    Pr[PKEROM.OW_PCVA(PKEROM.RO.LRO, TT, A0).main() @ &m : res] <=
-    Pr[OW_CPA(BasePKE, AdvOW(A0)).main() @ &m : res] +
-    (qH + qP)%r * Pr[OW_CPA(BasePKE, AdvOW_query(A0)).main() @ &m : res] +
-    (qH + qP + 2)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(A0), PKEROM.RO.RO)).main() @ &m : res] +
-    qV%r * gamma_spread.
-*)
+  Pr[OW_PCVA(RO.LRO, TT, A).main() @ &m : res] <=
+      2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(A)))).main() @ &m : res] - 1%r / 2%r| 
+    + 2%r * `| Pr[PKE.CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(A))).main() @ &m : res] - 1%r/2%r | 
+    + Pr[ PKE.Correctness_Adv(BasePKE,BOWp(BasePKE,AdvOW_query(A))).main() @ &m : res ]
+    + Pr[ PKE.Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(A))).main() @ &m : res]
+    + (qH + qP + 2)%r * Pr[ PKE.Correctness_Adv(BasePKE,B(AdvCorr(A),RO.RO)).main() @ &m : res ]
+    + qV%r * gamma_spread + 2%r * (qH + qP + 1)%r * eps_msg.
 
-(*
-lemma ow_ind &m : 
-   islossless S.kg => 
-   islossless S.enc =>
-   islossless S.dec =>
-   islossless A.find => 
-
-   Pr[ OW_CPA(S,A).main() @ &m : res ] <=
-      2%r * (eps_msg + 
-        `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |) + 
-             Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ].
 *)
 
 end section.
@@ -1362,10 +1329,10 @@ end section.
 section.
 
 declare module A <: CCA_ADV  {-CCA, -RO1.RO, -RO1.FRO, -RO2.RO, -PRF, -RF, -UU2, -OW_CPA,
-                    -RO1E.FunRO, -Gm2, -H2, -Gm3, -PKEROM.OW_PCVA, -H2BOWMod, 
+                    -RO1E.FunRO, -Gm2, -H2, -Gm3, -PKEROM.OW_PCVA, -H2BOWMod, -OWL_CPA,
                      -PKEROM.RO.RO, -PKEROM.RO.FRO, -Correctness_Adv1, -B,
                      -PKEROM.OW_PCVA, -Correctness_Adv1, -CountO, -O_AdvOW, -Gm, 
-                     -BOWp, -OWvsIND.Bow, -BasePKE, -AdvOW_query_MERGE, -OWvsIND_RO.RO.RO}.
+                     -BOWp, -OWvsIND.Bowl, -BasePKE}.
 
 lemma conclusion &m : 
   qH = qHU + 1 =>
@@ -1386,7 +1353,7 @@ lemma conclusion &m :
            (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUCI(A), PKEROM.RO.RO)).main() @ &m : res] + 
            (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(BUUOWMod(A)), PKEROM.RO.RO)).main() @ &m : res] +
                          Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(BUUOWMod(A)))).main() @ &m : res] +
-              2%r * `|Pr[CPA(BasePKE, OWvsIND.Bow(AdvOW(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| +
+              2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(BUUOWMod(A))))).main() @ &m : res] - 1%r / 2%r| +
                  (qHU + 1)%r * Pr[OW_CPA(BasePKE, AdvOW_query(BUUOWMod(A))).main() @ &m : res] +
                    2%r * eps_msg. 
   proof.
@@ -1438,15 +1405,15 @@ lemma conclusion_cpa &m :
   islossless H0.get2 => islossless A(H0, O).guess) =>
 
   `| Pr[ KEMROMx2.CCA(RO_x2(RO1.RO,RO2.RO), UU, A).main() @ &m : res ] - 1%r/2%r | <=
-     `|Pr [ J.IND(PRF,D(A)).main() @ &m : res ] - 
-         Pr [ J.IND(RF, D(A)).main() @ &m : res ]|  + 
+      2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(OWvsIND.BL(AdvOW(BUUOWMod(A))))).main() @ &m : res] - 1%r / 2%r| +
+      2%r * `|Pr[CPA(BasePKE, OWvsIND.Bowl(AdvOWL_query(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| +
            (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUC(A), PKEROM.RO.RO)).main() @ &m : res] +
            (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(BUUCI(A), PKEROM.RO.RO)).main() @ &m : res] + 
            (qHU + 3)%r * Pr[Correctness_Adv(BasePKE, B(AdvCorr(BUUOWMod(A)), PKEROM.RO.RO)).main() @ &m : res] +
                          Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW(BUUOWMod(A)))).main() @ &m : res] +
-                         Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW_query_MERGE(BUUOWMod(A)))).main() @ &m : res] +
-              2%r * `|Pr[CPA(BasePKE, OWvsIND.Bow(AdvOW(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| +
-              2%r * `|Pr[CPA(BasePKE, OWvsIND_RO.BowROM(AdvOW_query_MERGE(BUUOWMod(A)))).main() @ &m : res] - 1%r / 2%r| +
+                         Pr[Correctness_Adv(BasePKE, BOWp(BasePKE, AdvOW_query(BUUOWMod(A)))).main() @ &m : res] +
+           `|Pr [ J.IND(PRF,D(A)).main() @ &m : res ] - 
+               Pr [ J.IND(RF, D(A)).main() @ &m : res ]|  + 
                   2%r * (qHU + 2)%r * eps_msg. 
   proof.
   move => qhval qv0 qp0 qhphc qhcb A_ll.
@@ -1478,7 +1445,7 @@ lemma conclusion_cpa &m :
   have ? : Pr[PKEROM.OW_PCVA(RO1.RO, TT, BUUOWMod(A)).main() @ &m : res] = 
            Pr[PKEROM.OW_PCVA(PKEROM.RO.LRO, TT, BUUOWMod(A)).main() @ &m : res]
     by byequiv => //;proc;inline *;sim.
-
+move => *.
    smt().
 qed.
 
diff --git a/proof/security/PKE_ROM.ec b/proof/security/PKE_ROM.ec
index 99bd3fb0..6d8e8a02 100644
--- a/proof/security/PKE_ROM.ec
+++ b/proof/security/PKE_ROM.ec
@@ -173,6 +173,7 @@ module OW_CPA (S:Scheme, A: OW_CPA_ADV) = {
   }
 }.
 
+
 module BOWp(S : Scheme, A :  OW_CPA_ADV) : CORR_ADV = {
    var m'' : plaintext option
 
@@ -238,177 +239,41 @@ qed.
 
 end section.
 
-(* Ind implies ow for large message spaces *)
-
-theory OWvsIND.
-
-module Bow(A :  OW_CPA_ADV) : Adversary = {
-   var m0, m1  : plaintext
-   var m       : plaintext option
-   var pk      : pkey
+(* Ind implies ow for large message spaces. We present a stronger
+   result for list-returning adversaries and then refine to the
+   case where only one message is returned.  *)
 
-   proc choose(_pk : pkey) : plaintext * plaintext = {
-     pk <- _pk;
-     m0 <$ dplaintext;
-     m1 <$ dplaintext;
-     return (m0,m1);
-   }
-
-   proc guess(c : ciphertext) : bool = {
-      var b;
-      b <$ {0,1};
-      m <@ A.find(pk,c);
-      return if (m = Some m0) 
-             then false 
-             else if (m = Some m1) 
-                  then true 
-                  else b;
-   }
+module type OWL_CPA_ADV = {
+  proc find(pk : pkey, c:ciphertext) : plaintext list
 }.
 
-section.
-
-
-declare module S <: Scheme {-Bow, -BOWp, -OW_CPA}.
-declare module A <: OW_CPA_ADV {-S, -Bow, -BOWp, -OW_CPA}.
+module OWL_CPA (S:Scheme, A: OWL_CPA_ADV) = {
+  var pk : pkey
+  var sk : skey
+  var m  : plaintext
+  var cc : ciphertext
+  var l : plaintext list
 
-local module Aux = {
-  proc main0() : bool = {
-   var pk,sk,c,b;
-   (pk, sk) <@ S.kg();                                                
-   Bow.pk <- pk;                                                       
-   Bow.m0 <$ dplaintext;                                                
-   Bow.m1 <$ dplaintext;                                               
-   c <@ S.enc(pk, Bow.m0);                                                
-   b <$ {0,1};                                                        
-   Bow.m <@ A.find(Bow.pk, c);                                           
-   return if Bow.m = Some Bow.m0 then false else if Bow.m = Some Bow.m1 then true else b;
-  }
+  proc main() = {
+    (pk, sk) <@ S.kg();
+    m        <$ dplaintext;
+    cc       <@ S.enc(pk, m);
+    l       <@ A.find(pk,cc);
+    return (m \in l);
 
-  proc main1() : bool = {
-   var pk,sk,c,b;
-   (pk, sk) <@ S.kg();                                                
-   Bow.pk <- pk;                                                       
-   Bow.m0 <$ dplaintext;                                                
-   Bow.m1 <$ dplaintext;                                               
-   c <@ S.enc(pk, Bow.m1);                                                
-   b <$ {0,1};                                                        
-   Bow.m <@ A.find(Bow.pk, c);                                           
-   return if Bow.m = Some Bow.m0 then false else if Bow.m = Some Bow.m1 then true else b;
   }
-
 }.
 
-print glob Bow.
-pred bad(gB : glob Bow) = (gB.`1 = None \/ (gB.`1 <> Some gB.`2 /\ gB.`1 <> Some gB.`3)).
-
-lemma ow_ind &m : 
-   islossless S.kg => 
-   islossless S.enc =>
-   islossless S.dec =>
-   islossless A.find => 
-
-   Pr[ OW_CPA(S,A).main() @ &m : res ] <=
-      2%r * (eps_msg + 
-        `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |) + 
-             Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ].
-proof. 
-move => kg_ll enc_ll dec_ll A_ll. 
-have : Pr[ OW_CPA(S,A).main_perfect() @ &m : res ] <=
-      2%r * (eps_msg + 
-        `| Pr[CPA(S,Bow(A)).main() @ &m : res] - 1%r/2%r |); last 
- by move : (ow_perfect  S A &m A_ll enc_ll dec_ll);smt().
-
-rewrite RField.mulrDr -(pr_CPA_LR S (Bow(A)) &m kg_ll enc_ll); 1,2: by islossless.
-
-have -> : 
-  Pr[CPA_L(S, Bow(A)).main() @ &m : res] = 
-  Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] + 
-  Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ !bad (glob Bow)]
-by rewrite Pr[mu_split bad (glob Bow)] => /#.
-
-have -> : 
-  Pr[CPA_R(S, Bow(A)).main() @ &m : res] = 
-  Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] + 
-  Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ !bad (glob Bow)]
-by rewrite Pr[mu_split bad (glob Bow)] => /#.
 
-have ->  /=: 
-  Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)] =
-  Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ bad (glob Bow)].
-+ byequiv (: _ ==> (res /\ bad (glob Bow)){1} <=>
-                   (res /\ bad (glob Bow)){2}) => //.
-  proc. 
-  seq 2 2 : (={glob A, glob S, pk,sk, Bow.pk} /\ Bow.pk{1} = pk{1} /\
-             Bow.m0{1} = Bow.m1{2} /\ Bow.m1{1} = Bow.m0{2} /\ 
-             Bow.m0{1} = m0{1} /\ Bow.m1{1} = m1{1} /\
-             Bow.m0{2} = m0{2} /\ Bow.m1{2} = m1{2});
-     1: by inline *;swap {1} 4 1;auto;call(_: true); auto.
-  by inline *;wp;call(_: true);rnd;wp;call(_:true);auto => /> /#.
-  
-have H : 
-  `| Pr[OW_CPA(S, A).main_perfect() @ &m : res] - 
-      Pr[Aux.main1() @ &m : res /\ ! bad (glob Bow)]|  <=
-      Pr[Aux.main1() @ &m : Bow.m = Some Bow.m0 ].
-  + have -> : Pr[OW_CPA(S, A).main_perfect() @ &m : res] = 
-            Pr[Aux.main1()  @ &m : Bow.m = Some Bow.m1]
-     by byequiv => //;proc;inline*;wp;call(_: true);rnd{2};
-        call(:true);rnd;rnd{2};wp;call(_: true);auto => />.
-  byequiv : (Bow.m = Some Bow.m0) => //. 
-  proc;inline *.
-  by call(:true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#.
-
-have H0 : 
-   Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] <= eps_msg.
-+ have -> : Pr[CPA_L(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] = 
-            Pr[Aux.main0() @ &m : res /\ ! bad (glob Bow)]
-   by byequiv => //;proc;inline *;wp;conseq />; sim. 
-  byphoare => //. 
-  proc;inline *; swap 4 3.
-  conseq (: _ ==> Some Bow.m1 = Bow.m); 1: by smt().
-  seq 6 : true  (1%r)  (eps_msg) (0%r) (0%r).
-  + by trivial.
-  + by trivial. 
-  + rnd; skip => /> &hr.  
-    case(Bow.m{hr} = None); 1: by move => -> /=; rewrite mu0;smt(MFinT.card_gt0).
-    move => nnone.
-    have -> : (fun (x : plaintext) => Some x = Bow.m{hr})  = pred1 (oget Bow.m{hr}) 
-        by apply fun_ext => x;smt().
-    by smt(eps_msgE fun_ext).
-     + by hoare; trivial.
-  by trivial.
-
-have H1 : Pr[CPA_R(S, Bow(A)).main() @ &m : res /\ ! bad (glob Bow)] = 
-            Pr[Aux.main1() @ &m : res /\ ! bad (glob Bow)]
-      by byequiv => //;proc;inline*;wp;conseq />;sim.
-
-have  : Pr[Aux.main1() @ &m : Bow.m = Some Bow.m0] <= eps_msg; last by smt().
-byphoare => //. 
-proc;inline *;swap 3 4.
-conseq (: _ ==> Bow.m0 = oget Bow.m); 1: by smt().
-seq 6 : true  (1%r)  (eps_msg) (0%r) (0%r).
-+ by trivial.
-+ by islossless. 
-+ rnd; skip => />*; rewrite eps_msgE /#.
-+ by hoare; trivial. 
-by trivial. 
-qed.
-
-end section.
-
-end OWvsIND.
-
-(* Ind tightly implies even list OW for large message spaces *)
-
-theory OWvsIND_RO.
+theory OWvsIND.
 
-clone import FullRO as RO with
-   type in_t <- plaintext
-   proof *.
+(***)
+(***)
 
-module BowROM(A :  OW_CPA_ADV) : Adversary = {
+module Bowl(A :  OWL_CPA_ADV) : Adversary = {
    var m0, m1  : plaintext
    var pk      : pkey
+   var l       : plaintext list
 
    proc choose(_pk : pkey) : plaintext * plaintext = {
      pk <- _pk;
@@ -420,10 +285,10 @@ module BowROM(A :  OW_CPA_ADV) : Adversary = {
    proc guess(c : ciphertext) : bool = {
       var b;
       b <$ {0,1};
-      A.find(pk,c);
-      return if (m0 \in RO.m = m1 \in RO.m)
+      l <@ A.find(pk,c);
+      return if (m0 \in l = m1 \in l)
              then b
-             else if (m0 \in RO.m) 
+             else if (m0 \in l) 
                   then false 
                   else true;
    }
@@ -432,22 +297,22 @@ module BowROM(A :  OW_CPA_ADV) : Adversary = {
 section.
 
 
-declare module S <: Scheme {-BowROM, -BOWp, -OW_CPA}.
-declare module A <: OW_CPA_ADV {-S,  -BOWp, -OW_CPA, -BowROM}.
+declare module S <: Scheme {-Bowl, -BOWp, -OWL_CPA}.
+declare module A <: OWL_CPA_ADV {-S,  -BOWp, -OWL_CPA, -Bowl}.
 
 local module Aux = {
   proc main0() : bool = {
    var pk,sk,c,b;
    (pk, sk) <@ S.kg();                                                
-   BowROM.pk <- pk;                                                       
-   BowROM.m0 <$ dplaintext;                                                
-   BowROM.m1 <$ dplaintext;                                               
-   c <@ S.enc(pk, BowROM.m0);                                                
+   Bowl.pk <- pk;                                                       
+   Bowl.m0 <$ dplaintext;                                                
+   Bowl.m1 <$ dplaintext;                                               
+   c <@ S.enc(pk, Bowl.m0);                                                
    b <$ {0,1};                                                        
-   A.find(pk,c);
-   return if (BowROM.m0 \in RO.m = BowROM.m1 \in RO.m)
+   Bowl.l <@ A.find(pk,c);
+   return if (Bowl.m0 \in Bowl.l = Bowl.m1 \in Bowl.l)
           then b
-          else if (BowROM.m0 \in RO.m) 
+          else if (Bowl.m0 \in Bowl.l) 
                then false 
                else true;
   }
@@ -455,124 +320,130 @@ local module Aux = {
   proc main1() : bool = {
    var pk,sk,c,b;
    (pk, sk) <@ S.kg();                                                
-   BowROM.pk <- pk;                                                       
-   BowROM.m0 <$ dplaintext;                                                
-   BowROM.m1 <$ dplaintext;                                               
-   c <@ S.enc(pk, BowROM.m1);                                                
+   Bowl.pk <- pk;                                                       
+   Bowl.m0 <$ dplaintext;                                                
+   Bowl.m1 <$ dplaintext;                                               
+   c <@ S.enc(pk, Bowl.m1);                                                
    b <$ {0,1};                                                        
-   A.find(pk,c);
-   return if (BowROM.m0 \in RO.m = BowROM.m1 \in RO.m)
+   Bowl.l <@ A.find(pk,c);
+   return if (Bowl.m0 \in Bowl.l = Bowl.m1 \in Bowl.l)
           then b
-          else if (BowROM.m0 \in RO.m) 
+          else if (Bowl.m0 \in Bowl.l) 
                then false 
                else true;
   }
 
 }.
 
-print glob BowROM.
-pred bad(gB : glob BowROM) = (gB.`1 \in gB.`4 = gB.`2 \in gB.`4).
-lemma ow_ind_ro &m MAX : 
+lemma boundl l MAX :
+  0 <= MAX =>
+  mu dplaintext (fun (x : plaintext) => size l <= MAX /\ x \in l) <= MAX%r * eps_msg.
+proof. 
+case (!size l <= MAX) => *. 
++ by have -> : (fun (x : plaintext) => size l <= MAX /\ (x \in l)) = pred0;
+     rewrite ?mu0 /=;smt(MFinT.card_gt0).  
+have := Mu_mem.mu_mem_le_size l dplaintext eps_msg _.
++ move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni).  
+  rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq.
+  by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP).
+by have : (fun (x : plaintext) => size l <= MAX /\ (x \in l)) = 
+          (mem l); smt(MFinT.card_gt0).
+qed.
+
+print glob Bowl.
+pred bad(gB : glob Bowl) = (gB.`2 \in gB.`1 = gB.`3 \in gB.`1).
+lemma ow_ind_l &m MAX : 
    0 <= MAX =>
    islossless S.kg =>
    islossless S.enc =>
    islossless S.dec =>
    islossless A.find =>
 
-   hoare [ A.find : true ==> card (fdom RO.m) <= MAX ] =>
+   hoare [ A.find : true ==> size res <= MAX ] =>
 
-   Pr[ OW_CPA(S,A).main() @ &m :   OW_CPA.m \in RO.m] <=
+   Pr[ OWL_CPA(S,A).main() @ &m :   OWL_CPA.m \in OWL_CPA.l] <=
       2%r * (MAX%r * eps_msg + 
-        `| Pr[CPA(S,BowROM(A)).main() @ &m : res] - 1%r/2%r |).   
+        `| Pr[CPA(S,Bowl(A)).main() @ &m : res] - 1%r/2%r |).   
 proof. 
 move => max_ge0 kg_ll enc_ll dec_ll A_ll maxsize. 
 
-rewrite RField.mulrDr -(pr_CPA_LR S (BowROM(A)) &m kg_ll enc_ll); 1,2: by islossless.
+rewrite RField.mulrDr -(pr_CPA_LR S (Bowl(A)) &m kg_ll enc_ll); 1,2: by islossless.
 
 have -> : 
-  Pr[CPA_L(S, BowROM(A)).main() @ &m : res] = 
-  Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] + 
-  Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)]
-by rewrite Pr[mu_split bad (glob BowROM)] => /#.
+  Pr[CPA_L(S, Bowl(A)).main() @ &m : res] = 
+  Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] + 
+  Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)]
+by rewrite Pr[mu_split bad (glob Bowl)] => /#.
 
 have -> : 
-  Pr[CPA_R(S, BowROM(A)).main() @ &m : res] = 
-  Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] + 
-  Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)]
-by rewrite Pr[mu_split bad (glob BowROM)] => /#.
+  Pr[CPA_R(S, Bowl(A)).main() @ &m : res] = 
+  Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] + 
+  Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)]
+by rewrite Pr[mu_split bad (glob Bowl)] => /#.
 
 have ->  /=: 
-  Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)] =
-  Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ bad (glob BowROM)].
-+ byequiv (: ={glob A,glob S, RO.m} ==> (res /\ bad (glob BowROM)){1} <=>
-                   (res /\ bad (glob BowROM)){2}) => //.
+  Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)] =
+  Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ bad (glob Bowl)].
++ byequiv (: ={glob A,glob S, Bowl.l} ==> (res /\ bad (glob Bowl)){1} <=>
+                   (res /\ bad (glob Bowl)){2}) => //.
   proc. 
-  seq 2 2 : (={glob A, glob S, pk,sk, BowROM.pk,RO.m} /\ 
-         BowROM.m0{1} = BowROM.m1{2} /\ BowROM.m1{1} = BowROM.m0{2} /\ 
-         BowROM.pk{1} = pk{1} /\
-             BowROM.m0{1} = m0{1} /\ BowROM.m1{1} = m1{1} /\
-             BowROM.m0{2} = m0{2} /\ BowROM.m1{2} = m1{2});
+  seq 2 2 : (={glob A, glob S, pk,sk, Bowl.pk,Bowl.l} /\ 
+         Bowl.m0{1} = Bowl.m1{2} /\ Bowl.m1{1} = Bowl.m0{2} /\ 
+         Bowl.pk{1} = pk{1} /\
+             Bowl.m0{1} = m0{1} /\ Bowl.m1{1} = m1{1} /\
+             Bowl.m0{2} = m0{2} /\ Bowl.m1{2} = m1{2});
      1: by inline *; swap {1} 4 1;auto;call(_: true); auto. 
    by inline *;wp;call(_: true);rnd;wp;call(_:true);auto => /> /#.
 
-have H :   `| Pr[OW_CPA(S, A).main() @ &m : OW_CPA.m \in RO.m ] - 
-      Pr[Aux.main1() @ &m : res /\ ! bad (glob BowROM) ]|  <=
-         Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m].
-+ have -> : Pr[OW_CPA(S, A).main() @ &m : OW_CPA.m \in RO.m] = 
-       Pr[Aux.main1() @ &m : BowROM.m1 \in RO.m].
-  + byequiv (: ={glob A,glob S, RO.m} ==> _) => //. 
-    proc;inline*;wp;call{1}(_: true ==> true). 
-    by wp;call(:true); rnd{2};call(:true);rnd;rnd{2};wp;call(_: true);auto.
-  byequiv : (BowROM.m0 \in RO.m) => //. 
+have H :   `| Pr[OWL_CPA(S, A).main() @ &m : OWL_CPA.m \in OWL_CPA.l ] - 
+      Pr[Aux.main1() @ &m : res /\ ! bad (glob Bowl) ]|  <=
+         Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l].
++ have -> : Pr[OWL_CPA(S, A).main() @ &m : OWL_CPA.m \in OWL_CPA.l] = 
+       Pr[Aux.main1() @ &m : Bowl.m1 \in Bowl.l].
+  + byequiv => //. 
+    proc;inline*;wp. 
+    by wp;call(:true); rnd{2};call(:true);rnd;rnd{2};wp;call(_: true);auto => />.
+  byequiv : (Bowl.m0 \in Bowl.l) => //. 
   proc;inline *.
   by call(:true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#. 
 
 have H0 : 
-   Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ ! bad (glob BowROM)] <= MAX%r * eps_msg.
-+ have -> : Pr[CPA_L(S, BowROM(A)).main() @ &m : res /\ ! bad (glob BowROM)] = 
-            Pr[Aux.main0() @ &m : res /\ !bad (glob BowROM)].
-  + byequiv (:_ ==> ={res} /\ ((!bad (glob BowROM)){1} <=>(!bad (glob BowROM)){2})) => //; last by smt(). 
-    by proc;inline *;wp;conseq (_: _ ==> ={BowROM.m1, BowROM.m0, RO.m,b});[ by smt() | by sim ].  
-  have -> : Pr[Aux.main0() @ &m : res /\ ! bad (glob BowROM)] =
-      Pr[Aux.main0() @ &m : res /\ card (fdom RO.m) <= MAX /\ ! bad (glob BowROM)].
-  + have ?: `| Pr[Aux.main0() @ &m : res /\ !bad (glob BowROM)] -
-      Pr[Aux.main0() @ &m : res /\ card (fdom RO.m) <= MAX /\ !bad (glob BowROM)] | <= 0%r; last by smt().
-  + have ->: 0%r = Pr[Aux.main0() @ &m : ! card (fdom RO.m) <= MAX] 
+   Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ ! bad (glob Bowl)] <= MAX%r * eps_msg.
++ have -> : Pr[CPA_L(S, Bowl(A)).main() @ &m : res /\ ! bad (glob Bowl)] = 
+            Pr[Aux.main0() @ &m : res /\ !bad (glob Bowl)].
+  + byequiv (:_ ==> ={res} /\ ((!bad (glob Bowl)){1} <=>(!bad (glob Bowl)){2})) => //; last by smt(). 
+    by proc;inline *;wp;conseq (_: _ ==> ={Bowl.m1, Bowl.m0, Bowl.l,b});[ by smt() | by sim ].  
+  have -> : Pr[Aux.main0() @ &m : res /\ ! bad (glob Bowl)] =
+      Pr[Aux.main0() @ &m : res /\ size Bowl.l <= MAX /\ ! bad (glob Bowl)].
+  + have ?: `| Pr[Aux.main0() @ &m : res /\ !bad (glob Bowl)] -
+      Pr[Aux.main0() @ &m : res /\ size Bowl.l <= MAX /\ !bad (glob Bowl)] | <= 0%r; last by smt().
+  + have ->: 0%r = Pr[Aux.main0() @ &m : ! size Bowl.l <= MAX] 
      by  byphoare => //;hoare => /=;proc;inline *;call maxsize;auto => />. 
-    byequiv  : (!card (fdom RO.m) <= MAX) =>//.
+    byequiv  : (!size Bowl.l <= MAX) =>//.
     by proc;call(_: true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /> /#.
   byphoare => //. 
   proc;inline *; swap 4 3.
-  conseq (: _ ==> card (fdom RO.m) <= MAX /\ BowROM.m1 \in RO.m); 1: by smt().
+  conseq (: _ ==> size Bowl.l <= MAX /\ Bowl.m1 \in Bowl.l); 1: by smt().
   seq 6 : true  (1%r)  (MAX%r * eps_msg) (0%r) (0%r).
   + by trivial.
   + by trivial. 
-  + rnd; skip => /> &hr.  
-    case (!card (fdom RO.m{hr}) <= MAX) => *. 
-    + by have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = pred0;
-         rewrite ?mu0 /=;smt(MFinT.card_gt0). 
-    have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = (mem (fdom RO.m{hr})) 
-        by smt(mem_fdom).
-    have := Mu_mem.mu_mem_le (fdom RO.m{hr}) dplaintext eps_msg _; last by smt(MFinT.card_gt0). 
-    move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni).  
-    rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq.
-    by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP).
+  + by rnd; auto => /> *;apply boundl =>/#.  
   + by hoare; trivial.
   by trivial.
   
-have -> : Pr[CPA_R(S, BowROM(A)).main() @ &m : res /\ !bad (glob BowROM)] = 
-            Pr[Aux.main1()           @ &m : res /\ !bad (glob BowROM)].
-+ byequiv (: ={glob A,glob S, RO.m} ==> _) => //. 
+have -> : Pr[CPA_R(S, Bowl(A)).main() @ &m : res /\ !bad (glob Bowl)] = 
+            Pr[Aux.main1()           @ &m : res /\ !bad (glob Bowl)].
++ byequiv  => //. 
   by proc;inline*;wp;call(:true);rnd;wp;call(:true);wp;rnd;rnd;wp;call(:true);auto.
 
-have : Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] <= MAX%r * eps_msg; last by smt().
-have -> : Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] =
-      Pr[Aux.main1() @ &m : card (fdom RO.m) <= MAX /\ BowROM.m0 \in RO.m].
-+ have : `| Pr[Aux.main1() @ &m : BowROM.m0 \in RO.m] -
-    Pr[Aux.main1() @ &m : card (fdom RO.m) <= MAX /\ BowROM.m0 \in RO.m]| <= 0%r; last by smt().
-  + have ->: 0%r = Pr[Aux.main1() @ &m : ! card (fdom RO.m) <= MAX] 
+have : Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] <= MAX%r * eps_msg; last by smt().
+have -> : Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] =
+      Pr[Aux.main1() @ &m : size Bowl.l <= MAX /\ Bowl.m0 \in Bowl.l].
++ have : `| Pr[Aux.main1() @ &m : Bowl.m0 \in Bowl.l] -
+    Pr[Aux.main1() @ &m : size Bowl.l <= MAX /\ Bowl.m0 \in Bowl.l]| <= 0%r; last by smt().
+  + have ->: 0%r = Pr[Aux.main1() @ &m : ! size Bowl.l <= MAX] 
      by  byphoare => //;hoare => /=;proc;inline *;call maxsize;auto => />. 
-  byequiv : (!card (fdom RO.m) <= MAX) =>//.
+  byequiv : (!size Bowl.l <= MAX) =>//.
   by proc;call(_: true);rnd;call(:true);rnd;rnd;wp;call(:true);auto => /#.
 
 byphoare => //. 
@@ -580,23 +451,59 @@ proc;inline *; swap 3 4.
 seq 6 : true  (1%r)  (MAX%r * eps_msg) (0%r) (0%r).
 + by trivial.
 + by trivial. 
-+ rnd; skip => /> &hr.
-  case (!card (fdom RO.m{hr}) <= MAX) => *. 
-  + by have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = pred0;
-       rewrite ?mu0 /=;smt(MFinT.card_gt0). 
-  have -> : (fun (x : plaintext) => card (fdom RO.m{hr}) <= MAX /\ (x \in RO.m{hr})) = (mem (fdom RO.m{hr})) 
-      by smt(mem_fdom).
-  have := Mu_mem.mu_mem_le (fdom RO.m{hr}) dplaintext eps_msg _; last by smt(MFinT.card_gt0). 
-  move => *; rewrite mu1_uni; 1: by smt(dplaintext_uni).  
-  rewrite dplaintext_fu /= dplaintext_ll /eps_msg MFinT.card_size_to_seq.
-  by have -> : (support dplaintext) = predT; smt(dplaintext_fu is_fullP). 
++ by rnd; auto => /> *;apply boundl =>/#.  
 + by hoare; trivial.
 by trivial.
 qed.
 
 end section.
 
-end OWvsIND_RO.
+section.
+
+declare module S <: Scheme {-Bowl, -BOWp, -OW_CPA, -OWL_CPA}.
+declare module A <: OW_CPA_ADV {-S, -Bowl, -BOWp, -OW_CPA, -OWL_CPA}.
+
+module BL(A : OW_CPA_ADV) : OWL_CPA_ADV = {
+  proc find(pk : pkey, c : ciphertext) : plaintext list = {
+     var m';
+     m' <@ A.find(pk,c);
+     return if m' = None then [] else [oget m'];
+  }
+}.
+
+lemma ow_ind &m : 
+   islossless S.kg => 
+   islossless S.enc =>
+   islossless S.dec =>
+   islossless A.find => 
+
+   Pr[ OW_CPA(S,A).main() @ &m : res ] <=
+      2%r * (eps_msg + 
+        `| Pr[CPA(S,Bowl(BL(A))).main() @ &m : res] - 1%r/2%r |) + 
+             Pr[ Correctness_Adv(S,BOWp(S,A)).main() @ &m : res ].
+proof. 
+move => kg_ll enc_ll dec_ll A_ll. 
+have : Pr[ OW_CPA(S,A).main_perfect() @ &m : res ] <=
+      2%r * (eps_msg + 
+        `| Pr[CPA(S,Bowl(BL(A))).main() @ &m : res] - 1%r/2%r |); last 
+ by move : (ow_perfect  S A &m A_ll enc_ll dec_ll);smt().
+
+rewrite RField.mulrDr.
+
+have /= := ow_ind_l S (BL(A)) &m 1 _ kg_ll enc_ll dec_ll _ _ => //; 1: by islossless.
++ by proc;wp;call(_:true);auto;smt().
+
+have -> : Pr[OWL_CPA(S, BL(A)).main() @ &m : OWL_CPA.m \in OWL_CPA.l] = 
+          Pr[OW_CPA(S, A).main_perfect() @ &m : res]; last by smt().
+
+byequiv => //; proc;inline {1} 4; wp.
+conseq (: _ ==> OWL_CPA.m{1} = OW_CPA.m{2} /\ m'{1} = OW_CPA.m'{2}); 1: by auto => /> /#.
+by sim.
+qed.
+
+end section.
+
+end OWvsIND.
 
 
 end PKE.