update the subgoal as Manuel suggested.

Author: namasikanam

src/phl/ecPhlRnd.ml

@@ -464,31 +464,38 @@ module Core = struct
         let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
         f_and iscoupling_pred goal
       | Some `Left  ->
-        (* Goal: dmap d1 g = d2 => forall a, psi[x -> a, y -> g(a)] *)
+        (* Goal: dmap d1 g = d2 /\ forall a b, b = g(a) => psi[x -> a, y -> b] *)
         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_eq (f_app (f_op dmap_op [tyL; tyR] dmap_ty) [muL; g] tyR) muR in
 
         let a_id = EcIdent.create "a" in
+        let b_id = EcIdent.create "b" in
         let a = f_local a_id tyL in
+        let b = f_local b_id tyR in
         let post = es.es_po in
         let post_subst = subst_form_lv env (EcMemory.memory es.es_ml) lvL a post in
-        let post_subst = subst_form_lv env (EcMemory.memory es.es_mr) lvR (f_app_simpl g [a] tyR) post_subst in
+        let post_subst = subst_form_lv env (EcMemory.memory es.es_mr) lvR b post_subst in
 
-        let goal = f_forall_simpl [(a_id, GTty tyL)] post_subst in
+        let goal = f_imp (f_eq (f_app_simpl g [a] tyR) b) post_subst in
+        let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
         f_and dmap_pred goal
       | Some `Right ->
-        (* Goal: dmap d2 g = d1 => forall b, psi[y -> b, y -> g(b)] *)
+        (* Goal: dmap d2 g = d1 /\ forall a b, a = g(b) => psi[x -> a, y -> 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_eq (f_app (f_op dmap_op [tyR; tyL] dmap_ty) [muR; g] tyL) muL in
 
+        let a_id = EcIdent.create "a" in
         let b_id = EcIdent.create "b" in
+        let a = f_local a_id tyL in
         let b = f_local b_id tyR in
         let post = es.es_po in
-        let post_subst = subst_form_lv env (EcMemory.memory es.es_ml) lvL (f_app_simpl g [b] tyL) post in
+        let post_subst = subst_form_lv env (EcMemory.memory es.es_ml) lvL a post in
         let post_subst = subst_form_lv env (EcMemory.memory es.es_mr) lvR b post_subst in
-        let goal = f_forall_simpl [(b_id, GTty tyR)] post_subst in
+
+        let goal = f_imp (f_eq a (f_app_simpl g [b] tyL)) post_subst in
+        let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
         f_and dmap_pred goal
     in
     let goal = f_equivS_r { es with es_sl=sl'; es_sr=sr'; es_po=goal; } in