anchor.diff:      | ("op_Minus", [Constant (Int i)]) -> readback env (Constant (Int (Z.minus_big_int i)))
       | ("op_Addition", [Constant (Int i1); Constant (Int i2)]) -> readback env (Constant (Int (Z.add_big_int i1 i2)))
       | ("op_Subtraction", [Constant (Int i1); Constant (Int i2)]) -> readback env (Constant (Int (Z.sub_big_int i1 i2)))
  -    | ("op_GreaterThan", [Constant (Int i1); Constant (Int i2)]) -> readback env (Constant (Bool (Z.gt_big_int i2 i2)))
  +    | ("op_GreaterThan", [Constant (Int i1); Constant (Int i2)]) -> readback env (Constant (Bool (Z.gt_big_int i1 i2)))
       | ("equals", [typ; t1; t2]) -> readback env (Constant (Bool (readback env t1 = readback env t2)))
       | ("op_Negation", [Constant (Bool b)]) -> readback env (Constant (Bool (not b)))
  -    | ("c_and", [Constant (Bool b1); Constant (Bool b2)]) -> readback env (Constant (Bool (b1 && b2)))
  -    | ("c_or", [Constant (Bool b1); Constant (Bool b2)]) -> readback env (Constant (Bool (b1 || b2)))
  +    | ("l_and", [Constant (Bool b1); Constant (Bool b2)]) -> readback env (Constant (Bool (b1 && b2)))
  +    | ("l_or", [Constant (Bool b1); Constant (Bool b2)]) -> readback env (Constant (Bool (b1 || b2)))
  +    | ("b2t", [Constant (Bool b)]) -> readback env (Constant (Bool b))
       | _ -> failwith "Bad primitive op application"
   
   (* [readback] creates named binders and not De Bruijn *)
  
positive.code:   in
    let translated_type =
      match (SS.compress lb.lbtyp).n with
      | Tm_refine _ -> app (translate env bs lb.lbtyp) translated_def None // app (translate env (translated_def::bs) lb.lbtyp) translated_def None
      | _ -> Constant Unit
    in
    // VD: For debugging purposes, I'm forcing a readback here, but I don't think this is  necessary
    debug (fun () ->
            match (SS.compress lb.lbtyp).n with
            | Tm_refine _ ->
                let readback_type = readback env translated_type in
                BU.print2 "<<< Refinement for %s evaluates to %s\n" (t_to_string translated_def) (P.term_to_string readback_type)
            | _ -> ());
    make_univ_abst lb.lbunivs bs
  
  and translate (env:Env.env) (bs:list<t>) (e:term) : t =
  
negative.code:     | Refinement (b, r) ->
          let body = translate env [] (readback env r) in
          debug (fun () -> BU.print1 "Translated refinement body: %s\n" (t_to_string body));
          S.mk (Tm_refine(fst b, readback env body)) None Range.dummyRange
  
  // Zoe: Commenting out conflict with Danel
  // =======
  