fix

Author: namasikanam

src/phl/ecPhlRnd.ml

@@ -467,7 +467,7 @@ module Core = struct
         (* Goal: dmap d1 g = d2 => forall a, psi[x -> a, y -> g(a)] *)
         let dmap_op = EcPath.extend EcCoreLib.p_top ["Distr"; "dmap"] in
         let dmap_ty = tfun (tdistr tyL) (tfun (tfun tyL tyR) (tdistr tyR)) in
-        let dmap_pred = f_app (f_op dmap_op [tyL; tyR] dmap_ty) [muL; g; muR] tbool in
+        let dmap_pred = f_eq (f_app (f_op dmap_op [tyL; tyR] dmap_ty) [muL; g] tyR) muR in
 
         let a_id = EcIdent.create "a" in
         let a = f_local a_id tyL in
@@ -481,7 +481,7 @@ module Core = struct
         (* Goal: dmap d2 g = d1 => forall b, psi[y -> b, y -> g(b)] *)
         let dmap_op = EcPath.extend EcCoreLib.p_top ["Distr"; "dmap"] in
         let dmap_ty = tfun (tdistr tyR) (tfun (tfun tyR tyL) (tdistr tyL)) in
-        let dmap_pred = f_app (f_op dmap_op [tyR; tyL] dmap_ty) [muR; g; muL] tbool in
+        let dmap_pred = f_eq (f_app (f_op dmap_op [tyR; tyL] dmap_ty) [muR; g] tyL) muL in
 
         let b_id = EcIdent.create "b" in
         let b = f_local b_id tyR in