anchor.diff:                  (U.mk_app y [ S.as_arg (S.bv_to_name a2) ]))
               in
               mk_forall a1 (mk_forall a2 body)
  -    | Tm_arrow (binder :: binders, comp) -> //TODO: a bit confusing, since binders may be []
  +    | Tm_arrow (binder :: binders, comp) ->
  +        (* split away the first binder and recurse, so we fall in the case above *)
           let t = { t with n = Tm_arrow ([ binder ], S.mk_Total (U.arrow binders comp)) } in
           mk_rel t x y
  -    | Tm_arrow _ ->
  -        failwith "unhandled arrow"
  +    | Tm_arrow ([], _) ->
  +        failwith "impossible: arrow with empty binders"
       | _ ->
           (* TODO: assert that this is a base type. *)
           (* BU.print2 "base, x=%s, y=%s\n" (Print.term_to_string x) (Print.term_to_string y); *)
  
positive.code: // This function expects its argument [c] to be normalized and to satisfy [is_C c]
  and trans_F_ (env: env_) (c: typ) (wp: term): term =
    if not (is_C c) then
      failwith "not a C";
    let mk x = mk x None c.pos in
    match (SS.compress c).n with
    | Tm_app (head, args) ->
  
negative.code:       let r = is_C (fst (List.hd args)) in
        if r then begin
          if not (List.for_all (fun (h, _) -> is_C h) args) then
            raise_error (Error_UnexpectedDM4FType,
                           BU.format1 "Not a C-type (A * C): %s" (Print.term_to_string t))
                        t.pos;
          true
        end else begin
          if not (List.for_all (fun (h, _) -> not (is_C h)) args) then
            raise_error (Error_UnexpectedDM4FType,
                           BU.format1 "Not a C-type (C * A): %s" (Print.term_to_string t))
                        t.pos;
          false
        end
    | Tm_arrow (binders, comp) ->
        begin match nm_of_comp comp with
        | M t ->
            if (is_C t) then
              raise_error (Error_UnexpectedDM4FType,
                             BU.format1 "Not a C-type (C -> C): %s" (Print.term_to_string t))
                          t.pos;
            true
        | N t ->
            // assert (List.exists is_C binders) ==> is_C comp
  