anchor.diff:  let bind r1 env e1opt (lc1:lcomp) ((b, lc2):lcomp_with_binder) : lcomp =
     let lc1 = N.ghost_to_pure_lcomp env lc1 in //downgrade from ghost to pure, if possible
     let lc2 = N.ghost_to_pure_lcomp env lc2 in
  +  let joined_eff = join_lcomp env lc1 lc2 in
     if debug env Options.Extreme
     then
       (let bstr = match b with
  
positive.code:       let c = lc.comp() in
        if Util.is_ml_comp c then c
        else
          let close_wp u_res md res_t bvs wp0 =
            List.fold_right (fun x wp ->
                let bs = [mk_binder x] in
                let us = u_res::[env.universe_of env x.sort] in
                let wp = U.abs bs wp (Some (Inr (Const.effect_Tot_lid, [TOTAL]))) in
                mk_Tm_app (inst_effect_fun_with us env md md.close_wp) [S.as_arg res_t; S.as_arg x.sort; S.as_arg wp] None wp0.pos)
            bvs wp0 in
          let c = Normalize.unfold_effect_abbrev env c in
          let u_res_t, res_t, wp = destruct_comp c in
          let md = Env.get_effect_decl env c.effect_name in
          let wp = close_wp u_res_t md res_t bvs wp in
          mk_comp md u_res_t c.result_typ wp c.flags in
    {lc with comp=close}
  
  let maybe_assume_result_eq_pure_term env (e:term) (lc:lcomp) : lcomp =
    let refine () =
        let c = lc.comp() in
        if not (is_pure_or_ghost_effect env lc.eff_name)
        then c
        else if Util.is_partial_return c then c
        else if Util.is_tot_or_gtot_comp c
  
negative.code:         (match e1opt with | None -> "None" | Some e -> Print.term_to_string e)
          (Print.lcomp_to_string lc1) bstr (Print.lcomp_to_string lc2));
    let bind_it () =
        if env.lax then 
           let m = must (Env.effect_decl_opt env joined_eff) in
           let u_t = env.universe_of env lc2.res_typ in
           mk_comp m u_t lc2.res_typ S.tun []
        else begin
            let c1 = lc1.comp () in
            let c2 = lc2.comp () in
            if debug env Options.Extreme
            then Util.print5 "b=%s,Evaluated %s to %s\n And %s to %s\n"
                  (match b with
                    | None -> "none"
                    | Some x -> Print.bv_to_string x)
                  (Print.lcomp_to_string lc1)
                  (Print.comp_to_string c1)
                  (Print.lcomp_to_string lc2)
                  (Print.comp_to_string c2);
            let try_simplify () =
              let aux () =
                  if Util.is_trivial_wp c1
                  then match b with
                          | None -> Some (c2, "trivial no binder")
                          | Some _ ->
                              if Util.is_ml_comp c2 //|| not (Util.is_free [Inr x] (Util.freevars_comp c2))
                              then Some (c2, "trivial ml")
                              else None
                  else if Util.is_ml_comp c1 && Util.is_ml_comp c2
                  then Some (c2, "both ml")
                  else None
              in
              let subst_c2 reason =
                  match e1opt, b with
                      | Some e, Some x ->
                        Some (SS.subst_comp [NT(x,e)] c2, reason)
                      | _ -> aux()
              in
              if Util.is_total_comp c1
              && Util.is_total_comp c2
              then subst_c2 "both total"
              else if Util.is_tot_or_gtot_comp c1
                   && Util.is_tot_or_gtot_comp c2
              then Some (S.mk_GTotal (Util.comp_result c2), "both gtot")
              else match e1opt, b with
                  | Some e, Some x ->
                      if Util.is_total_comp c1 && not (Syntax.is_null_bv x)
                      then subst_c2 "substituted e"
                      else aux ()
                  | _ -> aux ()
            in
            match try_simplify () with
              | Some (c, reason) ->
                c
              | None ->
                let (md, a, kwp), (u_t1, t1, wp1), (u_t2, t2, wp2) = lift_and_destruct env c1 c2 in
                let bs = match b with
                  | None -> [null_binder t1]
                  | Some x -> [S.mk_binder x] in
                let mk_lam wp = U.abs bs wp (Some (Inr (Const.effect_Tot_lid, [TOTAL]))) in //we know it's total; let the normalizer reduce it
                let r1 = S.mk (S.Tm_constant (FStar.Const.Const_range r1)) None r1 in
                let wp_args = [S.as_arg r1; S.as_arg t1; S.as_arg t2; S.as_arg wp1; S.as_arg (mk_lam wp2)] in
                let k = SS.subst [NT(a, t2)] kwp in
                let wp = mk_Tm_app  (inst_effect_fun_with [u_t1;u_t2] env md md.bind_wp)  wp_args None t2.pos in
                let c = mk_comp md u_t2 t2 wp [] in
                c
          end
    in {eff_name=joined_eff;
        res_typ=lc2.res_typ;
        (* TODO : these cflags might be inconsistent with the one returned by bind_it  !!! *)
        cflags=[];
  