pub broadcast proof fn lemma_forall_seq_push<T>(s: Seq<T>, f: FnSpec<(int, T), bool>, v: T)Expand description
ensures
forall_seq(s, f) && f(s.len() as int, v) <==> #[trigger] forall_seq(s.push(v), f),forall_seq(s.push(v),f) is equivalent to forall_seq(s,f) and f(s.len(),v).