pub broadcast proof fn lemma_seq_all_push<T>(s: Seq<T>, f: FnSpec<(T,), bool>, v: T)Expand description
ensures
#[trigger] s.push(v).all(f) <==> s.all(f) && f(v),s.push(v).all(f)is equivalent tos.all(f)andf(v)`.