lemma_seq_all_drop_last

vstd_extra::seq_extra

Function lemma_seq_all_drop_last 

Source 
pub broadcast proof fn lemma_seq_all_drop_last<T>(s: Seq<T>, f: FnSpec<(T,), bool>)
Expand description
requires
s.len() > 0,
ensures
s.all(f) <==> #[trigger] s.drop_last().all(f) && f(s.last()),

s.all(f) is equivalent to s.drop_last().all(f) and f(s.last()).