anchor.diff:      | MLE_Record (_, fields) -> Util.for_all (fun (_, e) -> is_ml_value e) fields
       | _ -> false
   
  +//pre-condition: SS.compress t = Tm_abs _
  +//Collapses adjacent abstractions into a single n-ary abstraction
  +let normalize_abs (t0:term) : term =
  +    let rec aux bs t copt =
  +        let t = SS.compress t in
  +        match t.n with
  +            | Tm_abs(bs', body, copt) -> aux (bs@bs') body copt
  +            | _ ->
  +              let e' = U.unascribe t in
  +              if U.is_fun e'
  +              then aux bs e' copt
  +              else U.abs bs e' copt in
  +   aux [] t0 None
  +
  +let unit_binder = S.mk_binder <| S.new_bv None TypeChecker.Common.t_unit
   
   (*INVARIANT: we MUST always perform deep erasure after extraction of types, even when done indirectly e.g. translate_typ_of_arg below.
     Otherwise, there will be Ob.magic because the types get erased at some places and not at other places *)
  
positive.code:                 let when_opt, f_when = match when_opt with
                      | None -> None, E_PURE
                      | Some w -> 
                          let w, f_w, t_w = synth_exp env w in
                          let w = maybe_coerce env w t_w ml_bool_ty in
                          Some w, f_w in
                  let mlbranch, f_branch, t_branch = synth_exp env branch in
                  //Printf.printf "Extracted %s to %A\n" (Print.exp_to_string branch) mlbranch;
                  p |> List.map (fun (p, wopt) -> 
                      let when_clause = conjoin_opt wopt when_opt in
  
negative.code:             else e in
      (e, f, ty)
  
  (* maybe_coerce g e ty expect:
          Inserts an Obj.magic around e if ty </: expect
   *)
  let maybe_coerce (g:env) e ty (expect:mlty) : mlexpr  =
      let ty = eraseTypeDeep g ty in
      match type_leq_c g (Some e) ty expect with 
  