fn prove_negated_obligation<'tcx>(
    infcx: InferCtxt<'tcx>,
    o: &PredicateObligation<'tcx>,
    body_def_id: DefId
) -> bool