anchor.diff:  
   // [is_an_eta_expansion env vars body]:
   //       returns Some t'
  -//               if (fun xs -> t) is an eta-expansion of t'
  +//               if (fun xs -> body) is an eta-expansion of t'
   //       else returns None
   let is_an_eta_expansion env vars body =
       //assert vars <> []
  -    let rec aux t xs =
  +    let rec check_partial_applications t xs =
           match t.tm, xs with
           | App(app, [f; {tm=FreeV y}]), x::xs
             when (is_app app && Term.fv_eq x y) ->
  
positive.code:           then Some t
            else None
  
          | _ -> None in
    aux body (List.rev vars)
  
  (* [reify_body env t] assumes that [t] has a reifiable computation type *)
  (* that is env |- t : M t' for some effect M and type t' where M is reifiable *)
  
negative.code:           //t is of the form (ApplyTT f x)
            //   i.e., it's a partial or curried application of f to x
            //recurse on f with the remaining arguments
            check_partial_applications f xs
  
          | _, [] ->
            //Case 2:
            //We're left with a closed head term applied to no arguments.
            //This case is only reachable after unfolding the recursive calls in Case 1 (note vars <> [])
            //and checking that the body t is of the form (ApplyTT (... (ApplyTT t x0) ... xn))
  