Function concat_replicate

pub fn concat_replicate<T>(n: Int, m: Int, s: FSet<T>)

Distributivity of replicate over union.

logic

pearlite! {
    if n == 0 {
        concat_empty(s.replicate(m));
    } else {
        cons_concat::<T>();
        concat_replicate(n - 1, m, s);
    }
}

requires

0 <= n && 0 <= m

ensures

s.replicate(n + m) == FSet::concat(s.replicate(n), s.replicate(m))