anchor.diff:      let rest_bs =
         match (SS.compress ty).n with
         | Tm_arrow (bs, _) when List.length bs >= 2 ->
  -        (match SS.open_binders bs with
  -         | (a', _)::bs ->
  -           let bs, _ = List.splitAt (List.length bs - 1) bs in
  -           let substs = [NT (a', bv_to_name (fst a))] in
  -           SS.subst_binders substs bs
  -         | _ -> failwith "Impossible!")
  -      | _ -> raise_error (Errors.Fatal_UnexpectedEffect, "") r in  //AR: TODO: FIXME
  +        let ((a', _)::bs) = SS.open_binders bs in
  +        bs |> List.splitAt (List.length bs - 1) |> fst
  +           |> SS.subst_binders [NT (a', bv_to_name (fst a))]
  +      | _ -> not_an_arrow_error "stronger" 2 ty r in
       let bs = a::rest_bs in
  -    let f, g_f =
  +    let f, guard_f =
         let repr, g = fresh_repr r (Env.push_binders env bs) u (fst a |> S.bv_to_name) in
         S.gen_bv "f" None repr |> S.mk_binder, g in
  -    let ret_t, g_ret_t = fresh_repr r (Env.push_binders env bs) u (fst a |> S.bv_to_name) in
  +    let ret_t, guard_ret_t = fresh_repr r (Env.push_binders env bs) u (fst a |> S.bv_to_name) in
   
       let pure_wp_t =
         let pure_wp_ts = Env.lookup_definition [Env.NoDelta] env PC.pure_wp_lid |> must in
  
positive.code:     let rest_bs =
        match (SS.compress ty).n with
        | Tm_arrow (bs, _) when List.length bs >= 4 ->
          (match SS.open_binders bs with
           | (a', _)::(b', _)::bs ->
             let bs, _ = List.splitAt (List.length bs - 2) bs in
             let substs = [NT (a', bv_to_name (fst a)); NT (b', bv_to_name (fst b))] in
             SS.subst_binders substs bs
           | _ -> failwith "Impossible!")
        | _ -> raise_error (Errors.Fatal_UnexpectedEffect, "") r in  //AR: TODO: FIXME
      let bs = a::b::rest_bs in
      let f, g_f =
        let repr, g = fresh_repr r (Env.push_binders env bs) u_a (fst a |> S.bv_to_name) in
        S.gen_bv "f" None repr |> S.mk_binder, g in
      let g, g_g =
        let x_a = fresh_x_a "x" a in
        let repr, g = fresh_repr r (Env.push_binders env (bs@[x_a])) u_b (fst b |> S.bv_to_name) in
        S.gen_bv "g" None (U.arrow [x_a] (S.mk_Total' repr (Some u_b))) |> S.mk_binder, g in
      let repr, g_repr = fresh_repr r (Env.push_binders env bs) u_b (fst b |> S.bv_to_name) in
      let k = U.arrow (bs@[f; g]) (S.mk_Total' repr (Some u_b)) in
      let g_eq = Rel.teq env ty k in
      List.iter (Rel.force_trivial_guard env) [g_f; g_g; g_repr; g_eq];
      bind_us, bind_t, SS.close_univ_vars bind_us (N.normalize [Env.Beta] env k) in
  
    log_combinator "bind_repr" bind_repr;
  
    let stronger_repr =
      let stronger_repr = ed.stronger_repr |> must in
      let r = (snd stronger_repr).pos in
  
      let stronger_us, stronger_t, stronger_ty = check_and_gen' "stronger_repr" 1 None stronger_repr in
  
      if Env.debug env0 <| Options.Other "LayeredEffects" then
        BU.print2 "stronger combinator typechecked with term: %s and type: %s\n"
  
negative.code:     let a, u = fresh_a_and_u_a "a" in
      let rest_bs = TcUtil.layered_effect_indices_as_binders (sig_us, sig_t) u (a |> fst |> S.bv_to_name) in
      let bs = a::rest_bs in
      let k = U.arrow bs (S.mk_Total S.teff) in  //U.arrow does closing over bs
      let g_eq = Rel.teq env t k in
      Rel.force_trivial_guard env g_eq;
      sig_us, SS.close_univ_vars us (k |> N.remove_uvar_solutions env), sig_ty in
  
    log_combinator "signature" signature;
  
    (*
     * Effect repr
     *
     * The repr must have the type:
     *   a:Type -> <binders for effect indices> -> Type  //polymorphic in one universe (that of a)
     *)
    let repr =
      let r = (snd ed.repr).pos in
      let repr_us, repr_t, repr_ty = check_and_gen "repr" 1 ed.repr in
      
      let us, ty = SS.open_univ_vars repr_us repr_ty in
      let env = Env.push_univ_vars env0 us in
  