answer(forall_bound_check).