anchor.diff:          is |> List.map fst |> List.map (SS.subst substs)
         | _ -> raise_error (conjunction_t_error "f's type is not a repr type") r in
       List.fold_left2
  -      (fun g i1 f_i -> Env.conj_guard g (Rel.teq env i1 f_i))
  +      (fun g i1 f_i -> Env.conj_guard g (Rel.layered_effect_teq env i1 f_i (Some conjunction_name)))
         Env.trivial_guard is1 f_sort_is in
   
     let g_guard =
  
positive.code:   let _, bind_t = Env.inst_tscheme_with bind_t [u1; u2] in
  
    let bind_t_shape_error (s:string) =
      (Errors.Fatal_UnexpectedEffect, BU.format2
         "bind %s does not have proper shape (reason:%s)"
         (Print.term_to_string bind_t) s) in
  
    let a_b, b_b, rest_bs, f_b, g_b, bind_c =
      match (SS.compress bind_t).n with
  
negative.code: 
    let ct = U.comp_to_comp_typ c in
  
    let lift_name = BU.format2 "%s ~> %s" (string_of_lid ct.effect_name) (string_of_lid tgt) in
  
    let u, a, c_is = List.hd ct.comp_univs, ct.result_typ, ct.effect_args |> List.map fst in
  
    //lift_ts has the arrow type: <u>a:Type -> ..bs.. -> f -> repr a is
  