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