Fix some regressions from PR #789 (#820)

* fix printing logic for synchronized equivs

* fix `byequiv` with trivial precondition

Author: oskgo

src/ecReduction.ml

@@ -1825,7 +1825,7 @@ module EqTest = struct
   include EqMod_base(struct
     let for_expr env ~norm:_ alpha e1 e2 =
       let convert e =
-        let f = form_of_expr e in
+        let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in
 
         if Mid.is_empty alpha then f else
 

src/phl/ecPhlDeno.ml

@@ -436,7 +436,7 @@ let process_pre tc hyps prl prr pre post =
     let gen_r f = ss_inv_generalize_right f mr in
     let gen_l f = ss_inv_generalize_left  f ml in
     dof fl al ml pml gen_r; dof fr ar mr pmr gen_l;
-    map_ts_inv f_ands !eqs
+    map_ts_inv ~ml ~mr f_ands !eqs
 
 (* -------------------------------------------------------------------- *)
 let post_iff ml mr eq env evl evr =