lemma_forall_seq_drop_last

vstd_extra::seq_extra

Function lemma_forall_seq_drop_last 

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

forall_seq(s,f) is equivalent to forall_seq(s.drop_last(),f) and f(s.len() as int - 1, s.last()).