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