anchor.diff:          | Tm_refine(x, phi) ->
               if norm
               then (x.sort, Some(x, phi))
  -            else begin match norm_refinement env t1 with
  -                | {n=Tm_refine(x, phi)} -> (x.sort, Some(x, phi))
  -                | tt -> failwith (BU.format2 "impossible: Got %s ... %s\n" (Print.term_to_string tt) (Print.tag_of_term tt))
  -            end
  +            else (match norm_refinement env t1 with
  +                 | {n=Tm_refine(x, phi)} -> (x.sort, Some(x, phi))
  +                 | tt -> failwith (BU.format2 "impossible: Got %s ... %s\n"
  +                                               (Print.term_to_string tt)
  +                                               (Print.tag_of_term tt))
  +                 )
   
           | Tm_lazy i -> aux norm (U.unfold_lazy i)
   
  
positive.code:       let _ = if Env.debug env <| Options.Other "RelCheck"
                then let wl' = {wl with attempting=TProb eq_prob::sub_probs} in
                     BU.print1 "After meet/join refinements: %s\n" (wl_to_string wl') in
        begin
        match solve_t env eq_prob ({wl with attempting=sub_probs}) with
        | Success _ ->
           let wl = {wl with attempting=rest} in
           let wl = solve_prob' false (TProb tp) None [] wl in
           let _ = List.fold_left (fun wl p -> solve_prob' true p None [] wl) wl bounds_probs in
           solve env wl
        | Failed (p, msg) ->
           giveup env ("failed to solve sub-problems: " ^msg) (TProb tp)
        end
  
      | _ when flip -> failwith (BU.format1 "Impossible: Not a flex-rigid: %s" (prob_to_string env (TProb tp)))
  
negative.code:               | Some (t1, t2) -> SS.compress t1, SS.compress t2
                | None -> SS.compress t1, SS.compress t2
            in
            let t1, p1_opt = base_and_refinement_maybe_delta true env t1 in
            let t2, p2_opt = base_and_refinement_maybe_delta true env t2 in
            let p, wl = eq_prob t1 t2 wl in
            let t =
                match p1_opt, p2_opt with
                | Some (x, phi1), Some(y, phi2) ->
                  let x = freshen_bv x in
                  let subst = [DB(0, x)] in
                  let phi1 = SS.subst subst phi1 in
                  let phi2 = SS.subst subst phi2 in
                  U.refine x (op phi1 phi2)
  
                | None, Some (x, phi)
                | Some(x, phi), None ->
                  let x = freshen_bv x in
                  let subst = [DB(0, x)] in
                  let phi = SS.subst subst phi in
                  U.refine x (op U.t_true phi)
  
                | _ ->
                  t1
            in
            (t1, [p], wl)
      in
      let rec aux (out, probs, wl) ts =
          match ts with
  