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