anchor.diff:    | Tm_app (head, args) ->
         let t_head, s_head, u_head = check_n env head in
         let t_head = normalize t_head in
  -      let binders, comp = match (SS.compress t_head).n with
  -        | Tm_arrow (binders, comp) -> binders, comp
  -        | _ -> raise (Err (Util.format1 "%s: not a function type" (Print.term_to_string t_head)))
  +      let is_arrow t = match (SS.compress t).n with | Tm_arrow _ -> true | _ -> false in
  +      let rec flatten t = match (SS.compress t).n with
  +        | Tm_arrow (binders, { n = Total t }) when is_arrow t ->
  +            let binders', comp = flatten t in
  +            binders @ binders', comp
  +        | Tm_arrow (binders, comp) ->
  +            binders, comp
  +        | _ ->
  +            raise (Err (Util.format1 "%s: not a function type" (Print.term_to_string t_head)))
         in
  +      let binders, comp = flatten t_head in
         Util.print1 "[debug] type of [head] is %s\n" (Print.term_to_string t_head);
   
         // Making the assumption here that [Tm_arrow (..., Tm_arrow ...)]
  
positive.code:   // Making the assumption that the thing we're passed is a top-level name.
    match (SS.compress (N.normalize [ N.EraseUniverses ] env.env t)).n with
    | Tm_fvar { fv_name = lid } ->
        let t = N.normalize [ N.UnfoldUntil Delta_constant; N.NoInline ] env.env t in
        Util.print1 "Recording definition of %s\n" (text_of_lid lid.v);
        let keep, ret = f env t in
        { env with definitions = (lid.v, keep) :: env.definitions }, ret
  
negative.code:   let env, c_push = register env (mk_lid "push") c_push in
  
    let ret_tot_wp_a = Some (Inl (U.lcomp_of_comp (mk_Total wp_a))) in
    let mk_generic_app c =
      if List.length binders > 0 then
        mk (Tm_app (c, args_of_binders binders))
      else
        c
    in
  
    (* val st2_if_then_else : heap:Type -> a:Type -> c:Type0 ->
                              st2_wp heap a -> st2_wp heap a ->
  