lemma_seq_push_head_take_head

vstd_extra::seq_extra

Function lemma_seq_push_head_take_head 

Source 
pub broadcast proof fn lemma_seq_push_head_take_head<T>(s: Seq<T>, hd: T)
Expand description
ensures
#[trigger] seq![hd].add(s)[0] == hd,