anchor.diff:        match (SS.compress (g_b |> fst).sort).n with
         | Tm_app (_, _::is) ->
           is |> List.map fst |> List.map (SS.subst substs)
  -      | _ -> failwith "Impossible!" in  //AR: TODO: FIXME: raise error
  +      | _ -> raise_error (conjunction_t_error "g's type is not a repr type") r in
       List.fold_left2
         (fun g i2 g_i -> Env.conj_guard g (Rel.teq env i2 g_i))
         Env.trivial_guard is2 g_sort_is in
  
positive.code: 
  let fvar_const env lid =  S.fvar (Ident.set_lid_range lid (Env.get_range env)) delta_constant None
  
  let mk_layered_conjunction env (ed:S.eff_decl) (u_a:universe) (a:term) (p:typ) (ct1:comp_typ) (ct2:comp_typ) : comp * guard_t =
    let _, conjunction = Env.inst_tscheme_with (ed.match_wps |> right).conjunction [u_a] in
    let is1, is2 = List.map fst ct1.effect_args, List.map fst ct2.effect_args in
    let a_b, rest_bs, f_b, g_b, p_b, body =
      match (SS.compress conjunction).n with
      | Tm_abs (bs, body, _) when List.length bs >= 4 ->
        let (a_b::bs), body = SS.open_term bs body in
        let rest_bs, (f_b::g_b::p_b::[]) = List.splitAt (List.length bs - 3) bs in
        a_b, rest_bs, f_b, g_b, p_b, body |> U.unascribe
      | _ -> failwith "Impossible" in  //AR: TODO: FIXME: raise error 
  
    let rest_bs_uvars, g_uvars = Env.uvars_for_binders
      env rest_bs [NT (a_b |> fst, a)]
      (fun b -> BU.format3
        "implicit var for binder %s of %s:conjunction at %s"
        (Print.binder_to_string b) (Ident.string_of_lid ed.mname)
        (env |> Env.get_range |> Range.string_of_range)) (env |> Env.get_range) in  //TODO: FIXME: better range?
  
    let substs = List.map2
      (fun b t -> NT (b |> fst, t))
  
negative.code:  * Then we substitute [a/c1_a; b/c2_a] in <some binders>
   *
   * Next we create ?u1 ... ?un for each of the binders in <some binders>
   *   while substituting [bi/?ui] in subsequent binders (so that their sorts are well-typed)
   *
   * Let substs = [a/c1_a; b/c2_a; bi/?ui]
   *
  