anchor.diff:          * binders             (* binders from the abstraction checked against the binders in the corresponding Typ_fun, if any *)
           * binders             (* let rec binders, suitably guarded with termination check, if any *)
           * option<comp>        (* the expected comp type for the body *)
  -        * option<term>        (* a tactic to apply when checking the expected computation type *)
           * Env.env             (* environment for the body *)
           * term                (* the body itself *)
           * guard_t)            (* accumulated guard from checking the binders *)
  
positive.code:               | _ -> failwith "Impossible: Can't have a let rec annotation but no expected type"
            in
            let bs, envbody, g, _ = tc_binders env bs in
            let copt, tacopt, body, g = match (SS.compress body).n with
                | Tm_ascribed(e, (Inr c, tacopt), _) ->
                  let c, _, g' = tc_comp envbody c in
                  Some c, tc_tactic_opt envbody tacopt, body, Rel.conj_guard g g'
                | _ -> None, None, body, g
            in
            None, bs, [], copt, tacopt, envbody, body, g
  
        | Some t ->
            let t = SS.compress t in
  
negative.code:             | None -> f
              | Some tactic -> Rel.map_guard f (fun f -> Common.mk_by_tactic tactic (U.mk_squash f)) in
      let e, c, f2 = comp_check_expected_typ env e lc in
      let final_guard = Rel.conj_guard f f2 in
      e, c, final_guard
  
    | Tm_ascribed (e, (Inl t, topt), _) ->
      let k, u = U.type_u () in
  