Function lemma_seq_all_add Copy item path

pub broadcast proof fn lemma_seq_all_add<T>(s1: Seq<T>, s2: Seq<T>, f: FnSpec<(T,), bool>)

s1.all(f) && s2.all(f) <==> #[trigger] (s1 + s2).all(f),