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 fn =
                    if md.is_layered then mk_layered_conjunction
                    else mk_non_layered_conjunction in
                  let c, g_conjunction = fn env md u_res_t res_t g ct_then ct_else in
                  Some md,
                  c,
                  Env.conj_guard (Env.conj_guard (Env.conj_guard g_comp gthen) g_lift) g_conjunction
  
negative.code:   let is =
      match (SS.compress body).n with
      | Tm_app (_, a::args) -> List.map fst args
      | _ -> raise_error (conjunction_t_error "body is not a repr type") r in
  
    mk_Comp ({
      comp_univs = [u_a];
  