anchor.diff:  
       | Tm_app(e, args) ->
         (* Op("=!=", args) is desugared into Op("~", Op("==") and not resugared back as "=!=" *)
  +      let args, rest = remove_typechecker_added_args args in
         let resugar_as_app e args = 
           let args = args |> List.map (fun (e, qual) ->
                 resugar_term e) in
  
positive.code:     | Pat_wild _ -> true
      | _ -> false
  
  let rec resugar_term (t : S.term) : A.term =
      (* Cannot resugar term back to NamedTyp or Paren *)
      let mk (a:A.term') : A.term =
  
negative.code:             | [(a1, _);(a2, _)] -> a1, a2
              | _ -> failwith("wrong arguments to try_with") in
            (* where a1 and a1 is Tm_abs(Tm_match)) *)
            let decomp term = match (SS.compress term).n with
              | Tm_abs(x, e, _) ->
                let x, e = SS.open_term x e in
                e
              | _ -> failwith("unexpected") in
            let body = resugar_term (decomp body) in
            let handler = resugar_term (decomp handler) in
            let rec resugar_body t = match (t.tm) with
              | A.Match(e, [(_,_,b)]) -> b
              | A.Ascribed(t1, t2, t3) -> 
                (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
                mk (A.Ascribed(resugar_body t1, t2, t3))
              | _ -> failwith("unexpected body format") in
            let e = resugar_body body in
            let rec resugar_branches t = match (t.tm) with
              | A.Match(e, branches) -> branches
              | A.Ascribed(t1, t2, t3) -> 
                (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
                (* TODO: where should we keep the information stored in Ascribed? *)
                resugar_branches t1
              | _ -> 
                (* TODO: forall created by close_forall doesn't follow the normal forall format, not sure how to resugar back *)
                []
            in
            let branches = resugar_branches handler in
            mk (A.TryWith(e, branches))
  
          | Some op when op = "forall" || op = "exists" ->
  