pub broadcast proof fn lemma_seq_take_nothing<A>(s: Seq<A>, n: int)Expand description
ensures
n == 0 ==> (#[trigger] s[..n] =~= Seq::<A>::empty()),s[..0] is equivalent to the empty sequence.