Function seq_to_set_distributes_over_add

Source
pub proof fn seq_to_set_distributes_over_add<T>(s1: Seq<T>, s2: Seq<T>)
Expand description
ensures
s1.to_set() + s2.to_set() =~= (s1 + s2).to_set(),