lemma_seq_add_head_back

vstd_extra::seq_extra

Function lemma_seq_add_head_back 

Source 
pub broadcast proof fn lemma_seq_add_head_back<T>(s: Seq<T>)
Expand description
requires
s.len() > 0,
ensures
s =~= #[trigger] seq![s[0]].add(s.drop_first()),