Function set_produces_trans 

pub fn set_produces_trans<T: DeepModel, I: View<ViewTy = FSet<T::DeepModelTy>>>(
    a: I,
    ab: Seq<T>,
    b: I,
    bc: Seq<T>,
    c: I,
)

logic

requires

set_produces(a, ab, b)

requires

set_produces(b, bc, c)

ensures

set_produces(a, ab.concat(bc), c)