pub broadcast proof fn all_spec_ensures(r: Range<int>, p: FnSpec<(int,), bool>)Expand description
ensures
#[trigger] r.all_spec(p) ==> (forall |i| r.start <= i < r.end ==> #[trigger] p(i)),