Function bind_alive_regions 

fn bind_alive_regions<'tcx>(
    tcx: TyCtxt<'tcx>,
    def_id: DefId,
    property: &mut Property<'tcx>,
)

Bind Alive(p, 'a) region idents in a contract to Regions, resolving 'a against def_id (the item that declares 'a: the struct for its invariants, the function for its requires).