diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml
index 8b0a32851..2a67b979f 100644
--- a/src/phl/ecPhlDeno.ml
+++ b/src/phl/ecPhlDeno.ml
@@ -299,6 +299,8 @@ let t_equiv_deno_bad pre tc =
   let env, _hyps, concl = FApi.tc1_eflat tc in
   let fpr1, fpr2, fprb = tc_destr_deno_bad tc env concl in
   let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and prb = destr_pr fprb in
+  if not (pr2.pr_mem = prb.pr_mem) then
+    tc_error !!tc "invalid goal shape";
   let m = prb.pr_event.m in
   let ev2 = ss_inv_rebind pr2.pr_event m in
   let fand = map_ss_inv2 f_and ev2 (map_ss_inv1 f_not prb.pr_event) in
@@ -354,6 +356,8 @@ let t_equiv_deno_bad2 pre bad1 tc =
   let fpr1, fpr2, fprb = tc_destr_deno_bad2 tc env concl in
   let pr1 = destr_pr fpr1 and pr2 = destr_pr fpr2 and
       prb = destr_pr fprb in
+  if not (pr2.pr_mem = prb.pr_mem) then
+    tc_error !!tc "invalid goal shape";
   let f1 = pr1.pr_fun and f2 = pr2.pr_fun in
   let ev1 = pr1.pr_event and ev2 = pr2.pr_event in
   let ev1 = ss_inv_rebind ev1 bad1.m in
@@ -370,8 +374,8 @@ let t_equiv_deno_bad2 pre bad1 tc =
   let cpre = cond_pre env pr1 pr2 pre in
   let fpreb1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 bad1) in
   let fpren1 = f_pr pr1.pr_mem pr1.pr_fun pr1.pr_args (map_ss_inv2 f_and ev1 (map_ss_inv1 f_not bad1)) in
-  let fpreb2 = f_pr pr1.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 bad2) in
-  let fpren2 = f_pr pr1.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 (map_ss_inv1 f_not bad2)) in
+  let fpreb2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 bad2) in
+  let fpren2 = f_pr pr2.pr_mem pr2.pr_fun pr2.pr_args (map_ss_inv2 f_and ev2 (map_ss_inv1 f_not bad2)) in
   let fabs' =
     f_real_abs
       (f_real_sub (f_real_add fpreb1 fpren1) (f_real_add fpreb2 fpren2)) in