testcase

Author: namasikanam

tests/coupling-rnd.ec

@@ -87,6 +87,16 @@ proc.
 coupling{1} f.
 wp; skip => @/predT /=.
 + split.
-move => b ? a.
-smt().
-
+  + admit.
+(*   + apply eq_distr. *)
+(* rewrite dbiased1E. *)
+(* rewrite clamp_id. *)
+(* + exact mu_bounded. *)
+(* rewrite dmap1E /pred1 /(\o) /=. *)
+(* case b => _. *)
+(* + by apply mu_eq => x /#. *)
+(* rewrite (mu_eq _ _ (predC test)). *)
+(* + by smt(). *)
+(* by rewrite mu_not D_ll. *)
+  + by rewrite /f //.
+qed.