stop hardcoding the bound memory in program logic statements

Author: oskgo

examples/FundamentalLemma.ec

@@ -44,6 +44,6 @@ apply (ler_trans (max Pr[G1.main() @ &m: A (glob Mem) res /\ F (glob Mem) res]
                       Pr[G2.main() @ &m: B (glob Mem) res /\ F (glob Mem) res])).
 + smt(ge0_mu).
 have -> //: forall (x y x' y':real), x <= x' => y <= y' => max x y <= max x' y' by smt().
-+ by rewrite -(Pr_split G1 Mem F A &m) andbC; smt(ge0_mu).
-by rewrite -(Pr_split G2 Mem F B &m) andbC; smt(ge0_mu).
++ by rewrite -(Pr_split G1 Mem F A &m); smt(ge0_mu).  
+by rewrite -(Pr_split G2 Mem F B &m); smt(ge0_mu).
 qed.

examples/hashed_elgamal_generic.ec

@@ -260,7 +260,12 @@ section.
     by rewrite dt_ll DBool.dbool_ll.
   + by move=> H H_o_ll; proc; auto; call (guess_ll H _)=> //; auto=> />.
   + by move=> _; apply: dbits_ll.
-  by rewrite !eqT.
+  apply iffLR.
+  congr; 2:congr.
+  + byequiv (: ={glob OnBound.G0(D, LRO), arg} ==>
+               ={glob OnBound.G0(D, LRO), res}) => />; 1:sim.
+  byequiv (: ={glob OnBound.G1(D, LRO), arg} ==>
+             ={glob OnBound.G1(D, LRO), res}) => />; 1:sim.
   qed.
 
   local module G1' = {