anchor.diff:            | _ -> resugar_as_app e args
           end
   
  -      | Some "dtuple" when List.length args > 0 ->
  +      | Some ("dtuple", _) when List.length args > 0 ->
           (* this is desugared from Sum(binders*term) *)
           let args = last args in
           let body = match args with
  
positive.code:           | _ -> resugar_term t
          end
  
        | Some "try_with" when List.length args > 1 ->
          (* only the last two args are from original AST terms, others are added by typechecker *)
          (* TODO: we need a place to store the information in the args added by the typechecker *)
          let new_args = last_two args in
  
negative.code:         let branches = resugar_branches handler in
          mk (A.TryWith(e, branches))
  
        | Some ("try_with", _) ->
          resugar_as_app e args
  
        | Some (op, _) when op = "forall" || op = "exists" ->
          (* desugared from QForall(binders * patterns * body) to Tm_app(forall, Tm_abs(binders, Tm_meta(body, meta_pattern(list<args>)*)
          let rec uncurry xs pat (t:A.term) = match t.tm with
            | A.QExists(x, p , body)
  